option use-code-for-lists is missing

[arademaker]

SNARK already has built-in procedural attachments, in the form of rewrite code, for important arithmetical, symbolic, and list-processing functions. For instance, if there were no procedural attachment mechanism, the only way we would be able to add two numbers would be to reason from the axioms for addition, a rather ponderous business. However, if we select the option use-code-for-numbers, arithmetic operations will be carried out by the corresponding LISP code. In particular, a term (+ 2 2) will be immediately rewritten as 4, without invoking any axioms or inference rules. SNARK has procedural attachments for the principal arithmetic function and predicate symbols in the ANSI KIF COMMON LISP library. Similarly, selecting the options use-code-for-lists and use-code-for-characters will give SNARK access to ANSI KIF COMMON LISP's list and character libraries.

http://www.ai.sri.com/snark/tutorial/tutorial.html#htoc63

Does anyone know if the documentation is outdated or if the code is outdated regarding this tutorial?

[AtriyaSen]

As far as I know, the documentation is extremely outdated. - Sincerely, Atriya

via Newton Mail [https://cloudmagic.com/k/d/mailapp?ct=dx&cv=10.0.18&pv=10.14.6&source=email_footer_2] On Thu, Sep 12, 2019 at 11:30 AM, Alexandre Rademaker notifications@github.com wrote: SNARK already has built-in procedural attachments, in the form of rewrite code, for important arithmetical, symbolic, and list-processing functions. For instance, if there were no procedural attachment mechanism, the only way we would be able to add two numbers would be to reason from the axioms for addition, a rather ponderous business. However, if we select the option use-code-for-numbers, arithmetic operations will be carried out by the corresponding LISP code. In particular, a term (+ 2 2) will be immediately rewritten as 4, without invoking any axioms or inference rules. SNARK has procedural attachments for the principal arithmetic function and predicate symbols in the ANSI KIF COMMON LISP library. Similarly, selecting the options use-code-for-lists and use-code-for-characters will give SNARK access to ANSI KIF COMMON LISP's list and character libraries.

http://www.ai.sri.com/snark/tutorial/tutorial.html#htoc63 [http://www.ai.sri.com/snark/tutorial/tutorial.html#htoc63]

Does anyone know if the documentation is outdated or if the code is outdated regarding this tutorial?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub [https://github.com/nilqed/SNARK/issues/1?email_source=notifications&email_token=ACXGEWATNWZAQ4PJ53KOSMTQJKDDPA5CNFSM4IWIBVGKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HLCAERQ] , or mute the thread [https://github.com/notifications/unsubscribe-auth/ACXGEWG4KFSE2ST5X7ZKHGDQJKDDPANCNFSM4IWIBVGA] .

[nilqed]

You're right. The documentation has never been updated since Mark passed away 2013. Actually, status still is:

A guide to SNARK has been written:
  http://www.ai.sri.com/snark/tutorial/tutorial.html
but has not been updated yet to reflect changes in SNARK,
especially for temporal and spatial reasoning.

Indeed, I wasn't aware of use-code-for-lists, and I'm sure, there are a lot of other undocumented ones. Maybe we should collect such valuable contributions as yours in an addendum.

I was about to document all options in fricas_snark, however, time flies - I guess I've forgotten most of it ;-)

[nilqed]

Now I see the problem. Apparently there were some changes in the set-options functions between the 2008 and 2012 versions. That is, although use-code-for-lists has been mentioned in 20080805r038 it wasn't set yet (neither in the 2008 nor in the 2012 versions). I can't tell for the moment why it's mentioned in the manual. Maybe a declare-snark-option will do - I'll try to figure it out asap.

kfp@NUC MINGW64 /f/repos/snark-20120808r022/src
$ grep code-for-lists *.lisp
code-for-lists2.lisp:;;; File: code-for-lists2.lisp
code-for-lists2.lisp:(defun declare-code-for-lists ()
code-for-lists2.lisp:;;; code-for-lists2.lisp EOF
symbol-definitions.lisp:  (declare-code-for-lists)

kfp@NUC MINGW64 /f/repos/snark-20120808r022/src
$ cd ../../snark-20080805r038/src

kfp@NUC MINGW64 /f/repos/snark-20080805r038/src
$ grep code-for-lists *.lisp
code-for-lists2.lisp:;;; File: code-for-lists2.lisp
code-for-lists2.lisp:(defun declare-code-for-lists2 ()
code-for-lists2.lisp:;;; code-for-lists2.lisp EOF
options.lisp:  ;; e.g. for use-code-for-lists.
symbol-definitions.lisp:  (declare-code-for-lists2)

;;; 2008
(defun set-options (options)
  ;; ttp: 5/23/00 18:15 Do funcall instead of setting the symbol value
  ;; of the underlying variable so that "before" methods are invoked,
  ;; e.g. for use-code-for-lists.
  (assert-snark-option-specs-p options)
  (setf options-have-been-critiqued nil)
  (dolist (x options)
    (if (symbolp x)
        (funcall x t)
        (funcall (first x) (second x)))))

;;;; 2012
(defun set-options (options)
  (dolist (x options)
    (if (snark-option-spec-p x)
        (if (atom x) (funcall x t) (funcall (first x) (second x)))
        (warn "~S is not a SNARK option setting." x))))

[nilqed]

Declaring after loading seems to work. The symbols are actually defined in symbol-definitions.lisp: (declare-code-for-numbers), for instance. Before creating a patch I have to do some testing ... may take a while ;)

* (snark::declare-snark-option use-code-for-numbers t)
#<STANDARD-GENERIC-FUNCTION SNARK:USE-CODE-FOR-NUMBERS (1)>
* (use-code-for-numbers)

* (snark::use-code-for-numbers)
T

* (snark::print-options)
; The current SNARK option values are
;    (USE-RESOLUTION NIL)
;       (USE-HYPERRESOLUTION NIL)
;       (USE-NEGATIVE-HYPERRESOLUTION NIL)
;       (USE-UR-RESOLUTION NIL)
;       (USE-UR-PTTP NIL)
;       (USE-PARAMODULATION NIL)
;       (USE-FACTORING NIL)
;       (USE-EQUALITY-FACTORING NIL)
;       (USE-CONDENSING T)
;       (USE-RESOLVE-CODE NIL)
;       (USE-UNIT-RESTRICTION NIL)
;       (USE-INPUT-RESTRICTION NIL)
;       (USE-LITERAL-ORDERING-WITH-RESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-NEGATIVE-HYPERRESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-UR-RESOLUTION NIL)
;       (USE-LITERAL-ORDERING-WITH-PARAMODULATION NIL)
;       (USE-SUBSUMPTION T)
;       (USE-SUBSUMPTION-BY-FALSE :FALSE)
;       (USE-SIMPLIFICATION-BY-UNITS T)
;       (USE-SIMPLIFICATION-BY-EQUALITIES T)
;       (USE-TERM-ORDERING :RPO)
;       (USE-DEFAULT-ORDERING T)
;       (1-ARY-FUNCTIONS>2-ARY-FUNCTIONS-IN-DEFAULT-ORDERING NIL)
;       (ORDERING-FUNCTIONS>CONSTANTS NIL)
;       (RPO-STATUS :MULTISET)
;       (KBO-STATUS :LEFT-TO-RIGHT)
;       (USE-INDEFINITE-ANSWERS NIL)
;       (USE-CONDITIONAL-ANSWER-CREATION NIL)
;       (USE-CONSTRAINT-SOLVER-IN-SUBSUMPTION NIL)
;       (ALLOW-SKOLEM-SYMBOLS-IN-ANSWERS T)
;       (REWRITE-ANSWERS NIL)
;       (USE-CONSTRAINT-PURIFICATION NIL)
;       (USE-FUNCTION-CREATION NIL)
;       (USE-REPLACEMENT-RESOLUTION-WITH-X=X NIL)
;       (USE-PARAMODULATION-ONLY-INTO-UNITS NIL)
;       (USE-PARAMODULATION-ONLY-FROM-UNITS NIL)
;       (USE-SINGLE-REPLACEMENT-PARAMODULATION NIL)
;       (ASSERT-CONTEXT :ROOT)
;       (ASSERT-SUPPORTED T)
;       (ASSUME-SUPPORTED T)
;       (PROVE-SUPPORTED T)
;       (ASSERT-SEQUENTIAL NIL)
;       (ASSUME-SEQUENTIAL NIL)
;       (PROVE-SEQUENTIAL NIL)
;       (NUMBER-OF-GIVEN-ROWS-LIMIT NIL)
;       (NUMBER-OF-ROWS-LIMIT NIL)
;       (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT 10000)
;       (AGENDA-LENGTH-LIMIT 3000)
;       (RUN-TIME-LIMIT NIL)
;       (ROW-WEIGHT-LIMIT NIL)
;       (ROW-WEIGHT-BEFORE-SIMPLIFICATION-LIMIT NIL)
;       (LEVEL-PREF-FOR-GIVING NIL)
;       (AGENDA-ORDERING-FUNCTION SNARK:ROW-PRIORITY)
;       (PRUNING-TESTS (SNARK:ROW-WEIGHT-LIMIT-EXCEEDED))
;       (PRUNING-TESTS-BEFORE-SIMPLIFICATION (SNARK:ROW-WEIGHT-BEFORE-SIMPLIFICA
TION-LIMIT-EXCEEDED))
;       (USE-CLAUSIFICATION T)
;       (USE-EQUALITY-ELIMINATION NIL)
;       (USE-MAGIC-TRANSFORMATION NIL)
;       (USE-AC-CONNECTIVES T)
;       (USE-PURITY-TEST NIL)
;       (USE-RELEVANCE-TEST NIL)
;       (USE-CODE-FOR-NUMBERS T)
NIL
*

The definitions are in

$ grep code-for- *
code-for-bags4.lisp:;;; File: code-for-bags4.lisp
code-for-bags4.lisp:(defun declare-code-for-bags ()
code-for-bags4.lisp:;;; code-for-bags4.lisp EOF
code-for-lists2.lisp:;;; File: code-for-lists2.lisp
code-for-lists2.lisp:(defun declare-code-for-lists ()
code-for-lists2.lisp:;;; code-for-lists2.lisp EOF
code-for-numbers3.lisp:;;; File: code-for-numbers3.lisp
code-for-numbers3.lisp:(defun declare-code-for-numbers ()
code-for-numbers3.lisp:;;; code-for-numbers3.lisp EOF
code-for-strings2.lisp:;;; File: code-for-strings2.lisp
code-for-strings2.lisp:(defun declare-code-for-strings ()
code-for-strings2.lisp:;;; code-for-strings2.lisp EOF
date-reasoning2.lisp:(defun declare-code-for-dates ()
functions.lisp:      (setf (function-code-name0 symbol) (intern (to-string :code-for- (function-name symbol)) :keyword))))
main.lisp:                 :reason `(resolve ,row :code-for-$$eq))))))
symbol-definitions.lisp:  (declare-code-for-lists)
symbol-definitions.lisp:  (declare-code-for-bags)
symbol-definitions.lisp:  (declare-code-for-strings)
symbol-definitions.lisp:  (declare-code-for-numbers)
symbol-definitions.lisp:  (declare-code-for-dates)
tptp.lisp:       ((member :code-for-= (rrest x))
tptp.lisp:        (setf x (append (remove :code-for-= x) '(|theory(equality)|))))
tptp.lisp:   ((or (eq '|theory(equality)| x) (eq :code-for-= x))