diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-06-11 10:52:53 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-06-11 10:52:53 -0500 |
| commit | ee73990f8d383fc3848a44460b537667c4a2ce25 (patch) | |
| tree | ba6413da7b93e882da73027c710f7f43d7dd8f76 | |
| parent | 60007a036188c955d62de18c41be0b97f9b8413e (diff) | |
| parent | f10087c3b347da6ef625a2ad92846551ad324d73 (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new
96 files changed, 1370 insertions, 631 deletions
diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml index 761736e75..6632cbf45 100644 --- a/.github/workflows/docs_cleanup.yml +++ b/.github/workflows/docs_cleanup.yml @@ -44,15 +44,19 @@ jobs: SSH_AUTH_SOCK: /tmp/ssh_agent.sock run: | cd target - git log first=`git rev-list --max-parents=0 HEAD` last=`git rev-list --until=1.month.ago -n1 HEAD` if [ -n "$last" ]; then git checkout $last + ts=`git log -1 --format=%ct` git reset --soft $first - git commit -m "Squash old history" + if git diff --cached --exit-code + then + echo "Nothing to squash" + else + git commit -m "Squash old history" --date=$ts + fi git cherry-pick $last..main - git log fi - name: Push diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index ea3b2dde1..ecc6ce5fe 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -56,23 +56,23 @@ QF_LIA) finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_NIA) - trywith 480 --nl-ext-tplanes --decision=internal - trywith 60 --nl-ext-tplanes --decision=justification + trywith 420 --nl-ext-tplanes --decision=justification + trywith 60 --nl-ext-tplanes --decision=internal + trywith 60 --nl-ext-tplanes --decision=justification-old trywith 60 --no-nl-ext-tplanes --decision=internal trywith 60 --no-arith-brab --nl-ext-tplanes --decision=internal # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail - trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 300 --solve-int-as-bv=2 --bitblast=eager + trywith 300 --solve-int-as-bv=4 --bitblast=eager + trywith 300 --solve-int-as-bv=8 --bitblast=eager + trywith 300 --solve-int-as-bv=16 --bitblast=eager + trywith 600 --solve-int-as-bv=32 --bitblast=eager finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) - trywith 300 --nl-ext-tplanes --decision=internal - trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor - trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int - finishwith --nl-ext-tplanes --decision=justification + trywith 600 --decision=justification + trywith 300 --decision=internal --no-nl-cad --nl-ext=full --nl-ext-tplanes + finishwith --decision=internal --nl-ext=none ;; # all logics with UF + quantifiers should either fall under this or special cases below ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) @@ -139,14 +139,8 @@ QF_ABV) trywith 500 --arrays-weak-equiv finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv ;; -QF_UFBV) - # Benchmarks with uninterpreted sorts cannot be solved with eager - # bit-blasting currently - trywith 1200 --bitblast=eager --bv-sat-solver=cadical - finishwith - ;; -QF_BV) - finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction +QF_BV|QF_UFBV) + finishwith --bitblast=eager --bv-assert-input ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification @@ -162,8 +156,8 @@ QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; QF_S|QF_SLIA) - trywith 300 --strings-exp --rewrite-divk --strings-fmf --no-jh-rlv-order - finishwith --strings-exp --rewrite-divk --no-jh-rlv-order + trywith 300 --strings-exp --strings-fmf --no-jh-rlv-order + finishwith --strings-exp --no-jh-rlv-order ;; QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index e0b51bc46..21bb2f6e0 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -38,19 +38,19 @@ QF_AUFLIA) runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) - runcvc5 --incremental --bitblast=eager --bv-sat-solver=cadical + runcvc5 --incremental --bitblast=eager --bv-assert-input ;; QF_UFBV) - runcvc5 --incremental + runcvc5 --incremental --bv-assert-input ;; QF_UF) runcvc5 --incremental ;; QF_AUFBV) - runcvc5 --incremental + runcvc5 --incremental --bv-assert-input ;; QF_ABV) - runcvc5 --incremental + runcvc5 --incremental --bv-assert-input ;; ABVFP) runcvc5 --incremental diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation index b5df43b72..fe8d4ae44 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation @@ -20,7 +20,7 @@ QF_LIA) finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --pb-rewrites --ite-simp --simp-ite-compress ;; QF_BV) - finishwith --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --bv-assert-input ;; *) # just run the default diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index d87e83257..e9753781d 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -17,7 +17,7 @@ QF_LRA) finishwith --no-restrict-pivots --use-soi --new-prop ;; QF_LIA) - finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --ite-simp --simp-ite-compress + finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi ;; QF_NIA) finishwith --nl-ext --nl-ext-tplanes @@ -42,16 +42,16 @@ NIA|NRA) finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal ;; QF_AUFBV) - finishwith --decision=justification-stoponly --ite-simp + finishwith --decision=justification-stoponly ;; QF_ABV) - finishwith --ite-simp --simp-with-care --arrays-weak-equiv + finishwith --arrays-weak-equiv ;; QF_UFBV) finishwith ;; QF_BV) - finishwith --no-bv-abstraction + finishwith ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification diff --git a/docs/api/cpp/kind.rst b/docs/api/cpp/kind.rst index 579407c85..4c07804a4 100644 --- a/docs/api/cpp/kind.rst +++ b/docs/api/cpp/kind.rst @@ -4,14 +4,8 @@ Kind Every :cpp:class:`Term <cvc5::api::Term>` has a kind which represents its type, for example whether it is an equality (:cpp:enumerator:`EQUAL <cvc5::api::Kind::EQUAL>`), a conjunction (:cpp:enumerator:`AND -<cvc5::api::Kind::AND>`), or a bitvector addition -(:cpp:enumerator:`BITVECTOR_PLUS <cvc5::api::Kind::BITVECTOR_PLUS>`). -#ifndef DOXYGEN_SKIP -Note that the API type :cpp:enum:`cvc5::api::Kind` roughly corresponds to -:cpp:enum:`cvc5::Kind`, but is a different type. It hides internal kinds that -should not be exported to the API, and maps all kinds that we want to export -to its corresponding internal kinds. -#endif +<cvc5::api::Kind::AND>`), or a bit-vector addition +(:cpp:enumerator:`BITVECTOR_ADD <cvc5::api::Kind::BITVECTOR_ADD>`). .. doxygenenum:: cvc5::api::Kind :project: cvc5 diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index 528566a3e..5e17d524b 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -16,10 +16,11 @@ For every example, the same problem is constructed and solved using different in datatypes floatingpoint lineararith + relations sequences sets strings combination sygus-fun sygus-grammar - sygus-inv
\ No newline at end of file + sygus-inv diff --git a/docs/examples/relations.rst b/docs/examples/relations.rst new file mode 100644 index 000000000..d94fa0aa7 --- /dev/null +++ b/docs/examples/relations.rst @@ -0,0 +1,7 @@ +Theory of Relations +=================== + + +.. api-examples:: + ../../examples/api/smtlib/relations.smt2 + diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst index 71a6843c3..b0f1fc1da 100644 --- a/docs/examples/sets.rst +++ b/docs/examples/sets.rst @@ -5,3 +5,4 @@ Theory of Sets .. api-examples:: ../../examples/api/cpp/sets.cpp ../../examples/api/python/sets.py + ../../examples/api/smtlib/sets.smt2 diff --git a/docs/ext/examples.py b/docs/ext/examples.py index 003726de4..9f8f7294e 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -22,7 +22,7 @@ class APIExamples(Directive): '.cpp': {'title': 'C++', 'lang': 'c++'}, '.java': {'title': 'Java', 'lang': 'java'}, '.py': {'title': 'Python', 'lang': 'python'}, - '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'}, + '.smt2': {'title': 'SMT-LIBv2', 'lang': 'smtlib'}, } # The "arguments" are actually the content of the directive diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index 5dd54d006..e796e2404 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -7,15 +7,20 @@ class SmtLibLexer(RegexLexer): tokens = { 'root': [ + (r'ALL', token.Text), + (r'QF_ALL', token.Text), (r'QF_BV', token.Text), (r'QF_UFDT', token.Text), - (r'ALL_SUPPORTED', token.Text), + (r'QF_UFLIAFS', token.Text), + (r'set-info', token.Keyword), (r'set-logic', token.Keyword), (r'set-option', token.Keyword), (r'declare-codatatypes', token.Keyword), (r'declare-const', token.Keyword), + (r'declare-datatype', token.Keyword), (r'declare-datatypes', token.Keyword), (r'declare-fun', token.Keyword), + (r'declare-sort', token.Keyword), (r'define-fun', token.Keyword), (r'assert\b', token.Keyword), (r'check-sat-assuming', token.Keyword), @@ -32,14 +37,21 @@ class SmtLibLexer(RegexLexer): (r':produce-models', token.Name.Attribute), (r':produce-unsat-cores', token.Name.Attribute), (r':produce-unsat-assumptions', token.Name.Attribute), + (r':status', token.Name.Attribute), (r'!', token.Name.Attribute), + (r'Array', token.Name.Attribute), (r'BitVec', token.Name.Attribute), + (r'Int', token.Name.Attribute), (r'RNE', token.Name.Attribute), + (r'Set', token.Name.Attribute), + (r'String', token.Name.Attribute), (r'Tuple', token.Name.Attribute), + (r'tupSel', token.Name.Attribute), (r'true', token.String), (r'distinct', token.Operator), (r'=', token.Operator), (r'>', token.Operator), + (r'\*', token.Operator), (r'and', token.Operator), (r'bvadd', token.Operator), (r'bvashr', token.Operator), @@ -48,11 +60,30 @@ class SmtLibLexer(RegexLexer): (r'bvult', token.Operator), (r'bvule', token.Operator), (r'bvsdiv', token.Operator), + (r'card', token.Operator), + (r'emp', token.Operator), + (r'emptyset', token.Operator), + (r'exists', token.Operator), (r'extract', token.Operator), + (r'forall', token.Operator), (r'fp.gt', token.Operator), + (r'insert', token.Operator), + (r'intersection', token.Operator), (r'ite', token.Operator), + (r'member', token.Operator), (r'mkTuple', token.Operator), + (r'not', token.Operator), + (r'product', token.Operator), + (r'pto', token.Operator), + (r'sep', token.Operator), + (r'singleton', token.Operator), + (r'subset', token.Operator), + (r'tclosure', token.Operator), (r'to_fp_unsigned', token.Operator), + (r'transpose', token.Operator), + (r'union', token.Operator), + (r'univset', token.Operator), + (r'wand', token.Operator), (r'\+zero', token.Operator), (r'#b[0-1]+', token.Text), (r'bv[0-9]+', token.Text), @@ -67,5 +98,3 @@ class SmtLibLexer(RegexLexer): (r'\.\.\.', token.Text) ] } - - diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index 7dd0e8713..5f02a8bf8 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -179,7 +179,7 @@ a `cvc5::api::Solver solver` object. | | | | | | | ``Sort s = solver.mkTupleSort(sorts);`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ -| | ``(declare-const t (tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` | +| | ``(declare-const t (Tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` | | | | | | | | ``Sort s = solver.mkTypleSort({s_int, s_int});`` | | | | | diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst new file mode 100644 index 000000000..c2dcda78e --- /dev/null +++ b/docs/theories/separation-logic.rst @@ -0,0 +1,154 @@ +Theory Reference: Separation Logic +================================== + +cvc5 supports a syntax for separation logic as an extension of the SMT-LIB 2 +language. + +Signature +--------- + +Given a (decidable) base theory :math:`T`, cvc5 has a +`decision procedure <https://cvc4.github.io/publications/2016/RIS+16.pdf>`__ +for quantifier-free :math:`SL(T)_{Loc,Data}` formulas, where :math:`Loc` and +:math:`Data` are any sort belonging to :math:`T`. + +A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar: + +.. code:: + + F : L | (emp t u) | (pto t u) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op ... op Fn + +where ``op`` is any classical Boolean connective, ``t`` and ``u`` are terms +built from symbols in the signature of :math:`T` of sort :math:`Loc` and +:math:`Data` respectively, and :math:`L` is a :math:`T`-literal. + +The operator ``emp`` denotes the empty heap constraint, the operator ``pto`` +denotes the points-to predicate, the operator ``sep`` denotes separation start +and is variadic, and the operator ``wand`` denote magic wand. + +Semantics +--------- + +A satisfiability relation :math:`I,h \models_{SL} \varphi` is defined for +:math:`SL(T)_{Loc,Data}` formulas :math:`\varphi`, +where :math:`I` is an interpretation, and :math:`h` is a heap. + +The semantics of separation logic operators are as follows: + ++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+ +| :math:`I,h \models_{SL} L` | Iff | :math:`I \models L`, if :math:`L` is a :math:`T`-literal | ++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+ +| :math:`I,h \models_{SL}` (emp :math:`t \ u`) | Iff | :math:`h = \emptyset` | ++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+ +| :math:`I,h \models_{SL}` (pto :math:`t \ u`) | Iff | :math:`h = \{(t^I,u^I)\} \text{ and } t^I\not=nil^I` | ++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+ +| :math:`I,h \models_{SL}` (sep :math:`\phi_1 \ldots \phi_n)` | Iff | there exist heaps :math:`h_1,\ldots,h_n` s.t. :math:`h=h_1\uplus \ldots \uplus h_n` | +| | | | +| | | and :math:`I,h_i \models_{SL} \phi_i, i = 1,\ldots,n` | ++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+ +| :math:`I,h \models_{SL}` (wand :math:`\phi_1 \ \phi_2`) | Iff | for all heaps :math:`h'` if :math:`h'\#h` and :math:`I,h' \models_{SL} \phi_1` | +| | | | +| | | then :math:`I,h'\uplus h \models_{SL} \phi_2` | ++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+ + +where :math:`h_1 \uplus \ldots \uplus h_n` denotes the disjoint union of heaps +:math:`h_1, \ldots, h_n` and :math:`h'\#h` denotes that heaps :math:`h'` and +:math:`h` are disjoint, and :math:`nil` is a distinguished variable of sort +:math:`Loc`. +All classical Boolean connectives are interpreted as expected. + +.. note:: + The arguments of ``emp`` are used to denote the sort of the heap and have no + meaning otherwise. + +Syntax +------ + +Separation logic in cvc5 requires the ``QF_ALL`` logic. + +The syntax for the operators of separation logic is summarized in the following +table. +For the C++ API examples in this table, we assume that we have created +a :cpp:class:`cvc5::api::Solver` object. + ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Logic String | ``(set-logic QF_ALL)`` | ``solver.setLogic("QF_ALL");`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Empty Heap | ``(_ emp <Sort_1> <Sort_2>)`` | ``solver.mkTerm(Kind::SEP_EMP, x, y);`` | +| | | | +| | | where ``x`` and ``y`` are of sort ``<Sort_1>`` and ``<Sort_2>`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Points-To | ``(pto x y)`` | ``solver.mkTerm(Kind::SEP_PTO, x, y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Separation Star | ``(sep c1 .. cn)`` | ``solver.mkTerm(Kind::SEP_STAR, {c1, ..., cn});`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Magic Wand | ``(wand c1 c1)`` | ``solver.mkTerm(Kind::SEP_WAND, c1, c2);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Nil Element | ``(as nil <Sort>)`` | ``solver.mkSepNil(cvc5::api::Sort sort);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ + + +Examples +-------- + +The following input on heaps ``Int -> Int`` is unsatisfiable: + +.. code:: smtlib + + (set-logic QF_ALL) + (set-info :status unsat) + (declare-const x Int) + (declare-const a Int) + (declare-const b Int) + (assert (and (pto x a) (pto x b))) + (assert (not (= a b))) + (check-sat) + + +The following input on heaps ``U -> Int`` is satisfiable. Notice that the +formula ``(not (emp x 0))`` is satisfied by heaps ``U -> Int`` (the sorts of +``x`` and ``0`` respectively) whose domain is non-empty. + +.. code:: smtlib + + (set-logic QF_ALL) + (set-info :status sat) + (declare-sort U 0) + (declare-const x U) + (declare-const a Int) + (assert (and (not (_ emp U Int)) (pto x a))) + (check-sat) + +The following input on heaps ``Int -> Node`` is satisfiable, where ``Node`` +denotes a user-defined inductive `datatypes <datatypes>`__. + +.. code:: smtlib + + (set-logic QF_ALL) + (set-info :status sat) + (declare-const x Int) + (declare-const y Int) + (declare-const z Int) + (declare-datatype Node ((node (data Int) (left Int) (right Int)))) + (assert (pto x (node 0 y z))) + (check-sat) + +.. note:: + + Given a separation logic input, the sorts :math:`Loc` and :math:`Data` are + inferred by cvc5, and must be consistent across all predicates occurring in + an input. + cvc5 does not accept an input such as: + + .. code:: smtlib + + (set-logic QF_ALL) + (declare-sort U 0) + (declare-const x U) + (assert (and (pto x 0) (pto 1 2))) + (check-sat) + + since the sorts of the first arguments of the points-to predicates do not + agree. diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst new file mode 100644 index 000000000..79838334f --- /dev/null +++ b/docs/theories/sets-and-relations.rst @@ -0,0 +1,201 @@ +Theory Reference: Sets and Relations +==================================== + +Finite Sets +----------- + +cvc5 supports the theory of finite sets. +The simplest way to get a sense of the syntax is to look at an example: + +.. api-examples:: + ../../examples/api/cpp/sets.cpp + ../../examples/api/python/sets.py + ../../examples/api/smtlib/sets.smt2 + +The source code of these examples is available at: + +* `SMT-LIB 2 language example <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/sets.smt2>`__ +* `C++ API example <https://github.com/cvc5/cvc5/blob/master/examples/api/cpp/sets.cpp>`__ +* `Python API example <https://github.com/cvc5/cvc5/blob/master/examples/api/python/sets.cpp>`__ + + +Below is a short summary of the sorts, constants, functions and +predicates. For more details, see +`this paper at IJCAR 2016 <https://cvc4.github.io/publications/2016/BRBT16.pdf>`__. + +For the C++ API examples in the table below, we assume that we have created +a `cvc5::api::Solver solver` object. + ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Logic String | append `FS` for finite sets | append `FS` for finite sets | +| | | | +| | ``(set-logic QF_UFLIAFS)`` | ``solver.setLogic("QF_UFLIAFS");`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Sort | ``(Set <Sort>)`` | ``solver.mkSetSort(cvc5::api::Sort elementSort);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Constants | ``(declare-const X (Set Int)`` | ``Sort s = solver.mkSetSort(solver.getIntegerSort());`` | +| | | | +| | | ``Term X = solver.mkConst(s, "X");`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Union | ``(union X Y)`` | ``Term Y = solver.mkConst(s, "Y");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::UNION, X, Y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Intersection | ``(setminus X Y)`` | ``Term t = solver.mkTerm(Kind::SETMINUS, X, Y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Membership | ``(member x X)`` | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::MEMBER, x, X);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Subset | ``(subset X Y)`` | ``Term t = solver.mkTerm(Kind::SUBSET, X, Y);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Emptyset | ``(as emptyset (Set Int)`` | ``Term t = solver.mkEmptySet(s);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Singleton Set | ``(singleton 1)`` | ``Term t = solver.mkTerm(Kind::SINGLETON, solver.mkInteger(1));`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Cardinality | ``(card X)`` | ``Term t = solver.mkTerm(Kind::CARD, X);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Insert / Finite Sets | ``(insert 1 2 3 (singleton 4))`` | ``Term one = solver.mkInteger(1);`` | +| | | | +| | | ``Term two = solver.mkInteger(2);`` | +| | | | +| | | ``Term three = solver.mkInteger(3);`` | +| | | | +| | | ``Term sgl = solver.mkTerm(Kind::SINGLETON, solver.mkInteger(4));``| +| | | | +| | | ``Term t = solver.mkTerm(Kind::INSERT, {one, two, three, sgl});`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Complement | ``(complement X)`` | ``Term t = solver.mkTerm(Kind::COMPLEMENT, X);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ +| Universe Set | ``(as univset (Set Int))`` | ``Term t = solver.mkUniverseSet(s);`` | ++----------------------+----------------------------------------------+--------------------------------------------------------------------+ + + +Semantics +^^^^^^^^^ + +The semantics of most of the above operators (e.g., set union, intersection, +difference) are straightforward. +The semantics for the universe set and complement are more subtle and explained +in the following. + +The universe set ``(as univset (Set T))`` is *not* interpreted as the set +containing all elements of sort ``T``. +Instead it may be interpreted as any set such that all sets of sort ``(Set T)`` +are interpreted as subsets of it. +In other words, it is the union of the interpretations of all (finite) sets in +our input. + +For example: + +.. code:: smtlib + + (declare-fun x () (Set Int)) + (declare-fun y () (Set Int)) + (declare-fun z () (Set Int)) + (assert (member 0 x)) + (assert (member 1 y)) + (assert (= z (as univset (Set Int)))) + (check-sat) + +Here, a possible model is: + +.. code:: smtlib + + (define-fun x () (singleton 0)) + (define-fun y () (singleton 1)) + (define-fun z () (union (singleton 1) (singleton 0))) + +Notice that the universe set in this example is interpreted the same as ``z``, +and is such that all sets in this example (``x``, ``y``, and ``z``) are subsets +of it. + +The set complement operator for ``(Set T)`` is interpreted relative to the +interpretation of the universe set for ``(Set T)``, and not relative to the set +of all elements of sort ``T``. +That is, for all sets ``X`` of sort ``(Set T)``, the complement operator is +such that ``(= (complement X) (setminus (as univset (Set T)) X))`` +holds in all models. + +The motivation for these semantics is to ensure that the universe set for sort +``T`` and applications of set complement can always be interpreted as a finite +set in (quantifier-free) inputs, even if the cardinality of ``T`` is infinite. +Above, notice that we were able to find a model for the universe set of sort +``(Set Int)`` that contained two elements only. + +.. note:: + In the presence of quantifiers, cvc5's implementation of the above theory + allows infinite sets. + In particular, the following formula is SAT (even though cvc5 is not able to + say this): + + .. code:: smtlib + + (set-logic ALL) + (declare-fun x () (Set Int)) + (assert (forall ((z Int) (member (* 2 z) x))) + (check-sat) + + The reason for that is that making this formula (and similar ones) `unsat` is + counter-intuitive when quantifiers are present. + +Finite Relations +---------------- + +Example: + +.. api-examples:: + ../../examples/api/smtlib/relations.smt2 + +For reference, below is a short summary of the sorts, constants, functions and +predicates. +For more details, see +`this paper at CADE 2017 <https://cvc4.github.io/publications/2017/MRT+17.pdf>`__. + ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| | SMTLIB language | C++ API | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Logic String | ``(set-logic QF_ALL)`` | ``solver.setLogic("QF_ALL");`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Tuple Sort | ``(Tuple <Sort_1>, ..., <Sort_n>)`` | ``std::vector<cvc5::api::Sort> sorts = { ... };`` | +| | | | +| | | ``Sort s = solver.mkTupleSort(sorts);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| | ``(declare-const t (Tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` | +| | | | +| | | ``Sort s = solver.mkTypleSort({s_int, s_int});`` | +| | | | +| | | ``Term t = solver.mkConst(s, "t");`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Tuple Constructor | ``(mkTuple <Term_1>, ..., <Term_n>)`` | ``Sort s = solver.mkTypleSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term c = dt[0].getConstructor();`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Tuple Selector | ``((_ tupSel i) t)`` | ``Sort s = solver.mkTypleSort(sorts);`` | +| | | | +| | | ``Datatype dt = s.getDatatype();`` | +| | | | +| | | ``Term c = dt[0].getSelector();`` | +| | | | +| | | ``Term t = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Reation Sort | ``(Set (Tuple <Sort_1>, ..., <Sort_n>))`` | ``Sort s = solver.mkSetSort(cvc5::api::Sort tupleSort);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Constants | ``(declare-const X (Set (Tuple Int Int)`` | ``Sort s = solver.mkSetSort(solver.mkTupleSort({s_int, s_int});`` | +| | | | +| | | ``Term X = solver.mkConst(s, "X");`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Transpose | ``(transpose X)`` | ``Term t = solver.mkTerm(Kind::TRANSPOSE, X);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Transitive Closure | ``(tclosure X)`` | ``Term t = solver.mkTerm(Kind::TCLOSURE, X);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Join | ``(join X Y)`` | ``Term t = solver.mkTerm(Kind::JOIN, X, Y);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ +| Product | ``(product X Y)`` | ``Term t = solver.mkTerm(Kind::PRODUCT, X, Y);`` | ++----------------------+----------------------------------------------+------------------------------------------------------------------------------------+ diff --git a/docs/theory.rst b/docs/theory.rst index 45be41b2e..2d2a949d5 100644 --- a/docs/theory.rst +++ b/docs/theory.rst @@ -5,3 +5,5 @@ Theory References :maxdepth: 1 theories/datatypes + theories/separation-logic + theories/sets-and-relations diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index 5c9652707..c1eded4a4 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about sets with CVC4. + * A simple demonstration of reasoning about sets with cvc5. */ #include <cvc5/cvc5.h> diff --git a/examples/api/smtlib/relations.smt2 b/examples/api/smtlib/relations.smt2 new file mode 100644 index 000000000..11801a868 --- /dev/null +++ b/examples/api/smtlib/relations.smt2 @@ -0,0 +1,41 @@ +(set-logic ALL) +(set-info :status sat) + +(declare-fun r1 () (Set (Tuple String Int))) +(declare-fun r2 () (Set (Tuple Int String))) +(declare-fun r () (Set (Tuple String String))) +(declare-fun s () (Set (Tuple String String))) +(declare-fun t () (Set (Tuple String Int Int String))) +(declare-fun lt1 () (Set (Tuple Int Int))) +(declare-fun lt2 () (Set (Tuple Int Int))) +(declare-fun i () Int) + +(assert + (= r1 + (insert + (mkTuple "a" 1) + (mkTuple "b" 2) + (mkTuple "c" 3) + (singleton (mkTuple "d" 4))))) +(assert + (= r2 + (insert + (mkTuple 1 "1") + (mkTuple 2 "2") + (mkTuple 3 "3") + (singleton (mkTuple 17 "17"))))) +(assert (= r (join r1 r2))) +(assert (= s (transpose r))) +(assert (= t (product r1 r2))) +(assert + (= + lt1 + (insert + (mkTuple 1 2) + (mkTuple 2 3) + (mkTuple 3 4) + (singleton (mkTuple 4 5))))) +(assert (= lt2 (tclosure lt1))) +(assert (= i (card t))) + +(check-sat) diff --git a/examples/api/smtlib/sets.smt2 b/examples/api/smtlib/sets.smt2 new file mode 100644 index 000000000..437c285e2 --- /dev/null +++ b/examples/api/smtlib/sets.smt2 @@ -0,0 +1,34 @@ +(set-logic QF_UFLIAFS) +(set-option :produce-models true) +(set-option :incremental true) +(declare-const A (Set Int)) +(declare-const B (Set Int)) +(declare-const C (Set Int)) +(declare-const x Int) + +; Verify union distributions over intersection +(check-sat-assuming + ( + (distinct + (intersection (union A B) C) + (union (intersection A C) (intersection B C))) + ) +) + +; Verify emptset is a subset of any set +(check-sat-assuming + ( + (not (subset (as emptyset (Set Int)) A)) + ) +) + +; Find an element in {1, 2} intersection {2, 3}, if there is one. +(check-sat-assuming + ( + (member + x + (intersection + (union (singleton 1) (singleton 2)) + (union (singleton 2) (singleton 3)))) + ) +) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1831335ee..527912b8e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -52,6 +52,8 @@ libcvc5_add_sources( omt/omt_optimizer.h preprocessing/assertion_pipeline.cpp preprocessing/assertion_pipeline.h + preprocessing/learned_literal_manager.cpp + preprocessing/learned_literal_manager.h preprocessing/passes/ackermann.cpp preprocessing/passes/ackermann.h preprocessing/passes/apply_substs.cpp @@ -415,6 +417,8 @@ libcvc5_add_sources( theory/arith/nl/cad/cdcac_utils.h theory/arith/nl/cad/constraints.cpp theory/arith/nl/cad/constraints.h + theory/arith/nl/cad/lazard_evaluation.cpp + theory/arith/nl/cad/lazard_evaluation.h theory/arith/nl/cad/projections.cpp theory/arith/nl/cad/projections.h theory/arith/nl/cad/proof_checker.cpp diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 00308f11a..0e5d1d612 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -179,8 +179,8 @@ class CVC5_EXPORT Result bool isNotEntailed() const; /** - * Return true if query was a checkEntailed() () query and cvc5 was not able - * to determine if it is entailed. + * Return true if query was a checkEntailed() query and cvc5 was not able to + * determine if it is entailed. */ bool isEntailmentUnknown() const; @@ -2683,7 +2683,7 @@ class CVC5_EXPORT Statistics /** * Retrieve the statistic with the given name. * Asserts that a statistic with the given name actually exists and throws - * a `CVC4ApiRecoverableException` if it does not. + * a `CVC5ApiRecoverableException` if it does not. * @param name Name of the statistic. * @return The statistic with the given name. */ diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index b4596e977..2ec190360 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -33,9 +33,15 @@ namespace api { /** * The kind of a cvc5 term. * - * Note that the underlying type of Kind must be signed (to enable range - * checks for validity). The size of this type depends on the size of - * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h). + * \internal + * + * Note that the API type `cvc5::api::Kind` roughly corresponds to + * `cvc5::Kind`, but is a different type. It hides internal kinds that should + * not be exported to the API, and maps all kinds that we want to export to its + * corresponding internal kinds. The underlying type of `cvc5::api::Kind` must + * be signed (to enable range checks for validity). The size of this type + * depends on the size of `cvc5::Kind` (`NodeValue::NBITS_KIND`, currently 10 + * bits, see expr/node_value.h). */ enum CVC5_EXPORT Kind : int32_t { @@ -1844,9 +1850,10 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const` * - * Note: We currently support the creation of constant arrays, but under some + * @note We currently support the creation of constant arrays, but under some * conditions when there is a chain of equalities connecting two constant - * arrays, the solver doesn't know what to do and aborts (Issue <a href="https://github.com/CVC4/CVC4/issues/1667">#1667</a>). + * arrays, the solver doesn't know what to do and aborts (Issue <a + * href="https://github.com/cvc5/cvc5/issues/1667">#1667</a>). */ CONST_ARRAY, /** diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java index bd142b985..4399df1e4 100644 --- a/src/api/java/cvc5/Result.java +++ b/src/api/java/cvc5/Result.java @@ -122,7 +122,7 @@ public class Result extends AbstractPointer /** * Return true if query was a checkSat() or checkSatAssuming() query and - * CVC4 was not able to determine (un)satisfiability. + * cvc5 was not able to determine (un)satisfiability. */ public boolean isSatUnknown() { @@ -153,8 +153,8 @@ public class Result extends AbstractPointer private native boolean isNotEntailed(long pointer); /** - * Return true if query was a checkEntailed() () query and CVC4 was not able - * to determine if it is entailed. + * Return true if query was a checkEntailed() query and cvc5 was not able to + * determine if it is entailed. */ public boolean isEntailmentUnknown() { diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3339543f3..258005207 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -740,6 +740,21 @@ cdef class Solver: return term def mkReal(self, val, den=None): + ''' + Make a real number term. + + Really, makes a rational term. + + Can be used in various forms. + * Given a string "N/D" constructs the corresponding rational. + * Given a string "W.D" constructs the reduction of (W * P + D)/P, where + P is the appropriate power of 10. + * Given a float f, constructs the rational matching f's string + representation. This means that mkReal(0.3) gives 3/10 and not the + IEEE-754 approximation of 3/10. + * Given a string "W" or an integer, constructs that integer. + * Given two strings and/or integers N and D, constructs N/D. + ''' cdef Term term = Term(self) if den is None: term.cterm = self.csolver.mkReal(str(val).encode()) @@ -1766,12 +1781,14 @@ cdef class Term: return self.cterm.isRealValue() def getRealValue(self): - return float(Fraction(self.cterm.getRealValue().decode())) + '''Returns the value of a real term as a Fraction''' + return Fraction(self.cterm.getRealValue().decode()) def isBitVectorValue(self): return self.cterm.isBitVectorValue() def getBitVectorValue(self, base = 2): + '''Returns the value of a bit-vector term as a 0/1 string''' return self.cterm.getBitVectorValue(base).decode() def toPythonObj(self): diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 80d5bac57..61951841b 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -99,8 +99,8 @@ std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; } std::string Configuration::copyright() { std::stringstream ss; - ss << "Copyright (c) 2009-2020 by the authors and their institutional\n" - << "affiliations listed at http://cvc4.cs.stanford.edu/authors\n\n"; + ss << "Copyright (c) 2009-2021 by the authors and their institutional\n" + << "affiliations listed at https://cvc5.github.io/people.html\n\n"; if (Configuration::licenseIsGpl()) { ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n" @@ -185,7 +185,7 @@ std::string Configuration::copyright() { ss << "cvc5 is statically linked against these libraries. To recompile\n" "this version of cvc5 with different versions of these libraries\n" "follow the instructions on " - "https://github.com/CVC4/CVC4/blob/master/INSTALL.md\n\n"; + "https://github.com/cvc5/cvc5/blob/master/INSTALL.md\n\n"; } } diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h index e9169d9b2..4e7bde4b5 100644 --- a/src/decision/decision_engine_old.h +++ b/src/decision/decision_engine_old.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC4__DECISION__DECISION_ENGINE_OLD_H -#define CVC4__DECISION__DECISION_ENGINE_OLD_H +#ifndef CVC5__DECISION__DECISION_ENGINE_OLD_H +#define CVC5__DECISION__DECISION_ENGINE_OLD_H #include "base/output.h" #include "context/cdo.h" @@ -147,4 +147,4 @@ class DecisionEngineOld } // namespace cvc5 -#endif /* CVC4__DECISION__DECISION_ENGINE_H */ +#endif /* CVC5__DECISION__DECISION_ENGINE_H */ diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 82bfa1d70..52d6989c4 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -260,10 +260,9 @@ void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) // Notice we only want to do this for sygus datatypes that are user-provided. // At the moment, the condition !allow_all implies the grammar is // user-provided and hence may require a default constant. - // TODO (https://github.com/CVC4/cvc4-projects/issues/38): - // In an API for SyGuS, it probably makes more sense for the user to - // explicitly add the "any constant" constructor with a call instead of - // passing a flag. This would make the block of code unnecessary. + // For the SyGuS API, we could consider requiring the user to explicitly add + // the "any constant" constructor with a call instead of passing a flag. This + // would make the block of code unnecessary. if (allowConst && !allowAll) { // if I don't already have a constant (0-ary constructor) diff --git a/src/expr/node.h b/src/expr/node.h index fdcfcbe5f..5f5d3a976 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -126,7 +126,7 @@ typedef NodeTemplate<true> Node; * * More guidelines on when to use TNodes is available in the cvc5 * Developer's Guide: - * https://github.com/CVC4/CVC4/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes + * https://github.com/cvc5/cvc5/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes */ typedef NodeTemplate<false> TNode; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 1e6a38815..fe7d75ca3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -528,10 +528,6 @@ TypeNode NodeManager::mkBagType(TypeNode elementType) { CheckArgument( !elementType.isNull(), elementType, "unexpected NULL element type"); - CheckArgument(elementType.isFirstClass(), - elementType, - "cannot store types that are not first-class in bags. Try " - "option --uf-ho."); Debug("bags") << "making bags type " << elementType << std::endl; return mkTypeNode(kind::BAG_TYPE, elementType); } @@ -540,10 +536,6 @@ TypeNode NodeManager::mkSequenceType(TypeNode elementType) { CheckArgument( !elementType.isNull(), elementType, "unexpected NULL element type"); - CheckArgument(elementType.isFirstClass(), - elementType, - "cannot store types that are not first-class in sequences. Try " - "option --uf-ho."); return mkTypeNode(kind::SEQUENCE_TYPE, elementType); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index ad0593cee..b651c055a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1095,14 +1095,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, "unexpected NULL index type"); CheckArgument(!constituentType.isNull(), constituentType, "unexpected NULL constituent type"); - CheckArgument(indexType.isFirstClass(), - indexType, - "cannot index arrays by types that are not first-class. Try " - "option --uf-ho."); - CheckArgument(constituentType.isFirstClass(), - constituentType, - "cannot store types that are not first-class in arrays. Try " - "option --uf-ho."); Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); @@ -1111,10 +1103,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, inline TypeNode NodeManager::mkSetType(TypeNode elementType) { CheckArgument(!elementType.isNull(), elementType, "unexpected NULL element type"); - CheckArgument(elementType.isFirstClass(), - elementType, - "cannot store types that are not first-class in sets. Try " - "option --uf-ho."); Debug("sets") << "making sets type " << elementType << std::endl; return mkTypeNode(kind::SET_TYPE, elementType); } diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 5759ec856..6bdc1abc9 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -173,13 +173,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) } if (options::getDumpInstantiations(d_options) - && ((options::getInstFormatMode(d_options) - != options::InstFormatMode::SZS - && (res.isSat() - || (res.isSatUnknown() - && res.getUnknownExplanation() - == api::Result::INCOMPLETE))) - || isResultUnsat)) + && GetInstantiationsCommand::isEnabled(d_solver.get(), res)) { getterCommands.emplace_back(new GetInstantiationsCommand()); } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index caa0340bd..697501d13 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -57,7 +57,7 @@ thread_local Options* pOptions; const char* progPath; /** Just the basename component of argv[0] */ -const std::string* progName; +std::string progName; /** A pointer to the CommandExecutor (the signal handlers need it) */ std::unique_ptr<cvc5::main::CommandExecutor> pExecutor; @@ -80,7 +80,7 @@ TotalTimer::~TotalTimer() void printUsage(Options& opts, bool full) { stringstream ss; - ss << "usage: " << options::getBinaryName(opts) << " [options] [input-file]" + ss << "usage: " << progName << " [options] [input-file]" << endl << endl << "Without an input file, or with `-', cvc5 reads from standard input." @@ -106,13 +106,11 @@ int runCvc5(int argc, char* argv[], Options& opts) progPath = argv[0]; // Parse the options - vector<string> filenames = Options::parseOptions(&opts, argc, argv); + std::vector<string> filenames = + Options::parseOptions(&opts, argc, argv, progName); auto limit = install_time_limit(opts); - string progNameStr = options::getBinaryName(opts); - progName = &progNameStr; - if (opts.driver.help) { printUsage(opts, true); diff --git a/src/main/main.h b/src/main/main.h index 54abbdbe9..14d99f79c 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -34,7 +34,7 @@ class CommandExecutor; extern const char* progPath; /** Just the basename component of argv[0] */ -extern const std::string* progName; +extern std::string progName; /** A reference for use by the signal handlers to print statistics */ extern std::unique_ptr<cvc5::main::CommandExecutor> pExecutor; diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index d0628e2a7..b65600eb5 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -136,14 +136,14 @@ void segv_handler(int sig, siginfo_t* info, void* c) safe_print(STDERR_FILENO, "Spinning so that a debugger can be connected.\n"); safe_print(STDERR_FILENO, "Try: gdb "); - safe_print(STDERR_FILENO, *progName); + safe_print(STDERR_FILENO, progName); safe_print(STDERR_FILENO, " "); safe_print<int64_t>(STDERR_FILENO, getpid()); safe_print(STDERR_FILENO, "\n"); safe_print(STDERR_FILENO, " or: gdb --pid="); safe_print<int64_t>(STDERR_FILENO, getpid()); safe_print(STDERR_FILENO, " "); - safe_print(STDERR_FILENO, *progName); + safe_print(STDERR_FILENO, progName); safe_print(STDERR_FILENO, "\n"); for (;;) { @@ -191,14 +191,14 @@ void ill_handler(int sig, siginfo_t* info, void*) safe_print(STDERR_FILENO, "Spinning so that a debugger can be connected.\n"); safe_print(STDERR_FILENO, "Try: gdb "); - safe_print(STDERR_FILENO, *progName); + safe_print(STDERR_FILENO, progName); safe_print(STDERR_FILENO, " "); safe_print<int64_t>(STDERR_FILENO, getpid()); safe_print(STDERR_FILENO, "\n"); safe_print(STDERR_FILENO, " or: gdb --pid="); safe_print<int64_t>(STDERR_FILENO, getpid()); safe_print(STDERR_FILENO, " "); - safe_print(STDERR_FILENO, *progName); + safe_print(STDERR_FILENO, progName); safe_print(STDERR_FILENO, "\n"); for (;;) { diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index 34605cc71..0b62c0816 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -36,13 +36,12 @@ class OMTOptimizerInteger : public OMTOptimizer private: /** * Handles the optimization query specified by objType - * isMinimize = true will trigger minimization, + * isMinimize = true will trigger minimization, * otherwise trigger maximization **/ - smt::OptimizationResult optimize( - SmtEngine* optChecker, - TNode target, - bool isMinimize); + smt::OptimizationResult optimize(SmtEngine* optChecker, + TNode target, + bool isMinimize); }; } // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index 08f1809ec..2145492db 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node) } std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective( - OptimizationObjective& objective) + const OptimizationObjective& objective) { // the datatype of the target node TypeNode objectiveType = objective.getTarget().getType(true); @@ -53,7 +53,10 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective( } Node OMTOptimizer::mkStrongIncrementalExpression( - NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective) + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " @@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression( Unreachable(); } -Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, - TNode lhs, - TNode rhs, - OptimizationObjective& objective) +Node OMTOptimizer::mkWeakIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 1052865b0..1e8d9e763 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -46,7 +46,7 @@ class OMTOptimizer * and this is the optimizer for targetNode **/ static std::unique_ptr<OMTOptimizer> getOptimizerForObjective( - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Given the lhs and rhs expressions, with an optimization objective, @@ -70,7 +70,7 @@ class OMTOptimizer NodeManager* nm, TNode lhs, TNode rhs, - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Given the lhs and rhs expressions, with an optimization objective, @@ -94,7 +94,7 @@ class OMTOptimizer NodeManager* nm, TNode lhs, TNode rhs, - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Minimize the target node with constraints encoded in optChecker diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 7b2cde54a..f9d1c1a18 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -2,11 +2,6 @@ id = "BASE" name = "Base" [[option]] - name = "binary_name" - category = "undocumented" - type = "std::string" - -[[option]] name = "in" category = "undocumented" type = "std::istream*" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index fcad51ceb..8d4c2b1de 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -191,22 +191,6 @@ name = "Bitvector Theory" help = "simplify formula via Gaussian Elimination if applicable" [[option]] - name = "bvLazyRewriteExtf" - category = "regular" - long = "bv-lazy-rewrite-extf" - type = "bool" - default = "true" - help = "lazily rewrite extended functions like bv2nat and int2bv" - -[[option]] - name = "bvLazyReduceExtf" - category = "regular" - long = "bv-lazy-reduce-extf" - type = "bool" - default = "false" - help = "reduce extended functions like bv2nat and int2bv at last call instead of full effort" - -[[option]] name = "bvAlgExtf" category = "regular" long = "bv-alg-extf" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d06c64517..c1c843802 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -252,26 +252,29 @@ void OptionsHandler::setStats(const std::string& option, bool value) throw OptionException(ss.str()); } #endif /* CVC5_STATISTICS_ON */ - Assert(option.substr(0, 2) == "--"); - std::string opt = option.substr(2); + std::string opt = option; + if (option.substr(0, 2) == "--") + { + opt = opt.substr(2); + } if (value) { - if (option == options::base::statisticsAll__name) + if (opt == options::base::statisticsAll__name) { d_options->base.statistics = true; } - else if (option == options::base::statisticsEveryQuery__name) + else if (opt == options::base::statisticsEveryQuery__name) { d_options->base.statistics = true; } - else if (option == options::base::statisticsExpert__name) + else if (opt == options::base::statisticsExpert__name) { d_options->base.statistics = true; } } else { - if (option == options::base::statistics__name) + if (opt == options::base::statistics__name) { d_options->base.statisticsAll = false; d_options->base.statisticsEveryQuery = false; diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp index 7d72496aa..35e891f5a 100644 --- a/src/options/options_public.cpp +++ b/src/options/options_public.cpp @@ -103,10 +103,6 @@ int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; } std::istream* getIn(const Options& opts) { return opts.base.in; } std::ostream* getErr(const Options& opts) { return opts.base.err; } std::ostream* getOut(const Options& opts) { return opts.base.out; } -const std::string& getBinaryName(const Options& opts) -{ - return opts.base.binary_name; -} void setInputLanguage(InputLanguage val, Options& opts) { diff --git a/src/options/options_public.h b/src/options/options_public.h index 9b549601f..1d2f9edba 100644 --- a/src/options/options_public.h +++ b/src/options/options_public.h @@ -55,7 +55,6 @@ int32_t getVerbosity(const Options& opts) CVC5_EXPORT; std::istream* getIn(const Options& opts) CVC5_EXPORT; std::ostream* getErr(const Options& opts) CVC5_EXPORT; std::ostream* getOut(const Options& opts) CVC5_EXPORT; -const std::string& getBinaryName(const Options& opts) CVC5_EXPORT; void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT; void setOut(std::ostream* val, Options& opts) CVC5_EXPORT; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 0d6b7f01b..e909a5f0a 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -364,7 +364,8 @@ public: */ std::vector<std::string> Options::parseOptions(Options* options, int argc, - char* argv[]) + char* argv[], + std::string& binaryName) { Assert(options != NULL); Assert(argv != NULL); @@ -386,7 +387,7 @@ std::vector<std::string> Options::parseOptions(Options* options, if(x != NULL) { progName = x + 1; } - options->base.binary_name = std::string(progName); + binaryName = std::string(progName); std::vector<std::string> nonoptions; options->parseOptionsRecursive(argc, argv, &nonoptions); diff --git a/src/options/options_template.h b/src/options/options_template.h index 76c599d23..e9a4a6999 100644 --- a/src/options/options_template.h +++ b/src/options/options_template.h @@ -174,7 +174,8 @@ public: */ static std::vector<std::string> parseOptions(Options* options, int argc, - char* argv[]); + char* argv[], + std::string& binaryName); /** * Get the setting for all options. diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp new file mode 100644 index 000000000..fa6a01791 --- /dev/null +++ b/src/preprocessing/learned_literal_manager.cpp @@ -0,0 +1,52 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Learned literal manager + */ + +#include "preprocessing/learned_literal_manager.h" + +#include "theory/rewriter.h" + +namespace cvc5 { +namespace preprocessing { + +LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls, + context::UserContext* u, + ProofNodeManager* pnm) + : d_topLevelSubs(tls), d_learnedLits(u) +{ +} + +void LearnedLiteralManager::notifyLearnedLiteral(TNode lit) +{ + d_learnedLits.insert(lit); + Trace("pp-llm") << "LLM:notifyLearnedLiteral: " << lit << std::endl; +} + +std::vector<Node> LearnedLiteralManager::getLearnedLiterals() const +{ + std::vector<Node> currLearnedLits; + for (const auto& lit: d_learnedLits) + { + // update based on substitutions + Node tlsNode = d_topLevelSubs.get().apply(lit); + tlsNode = theory::Rewriter::rewrite(tlsNode); + currLearnedLits.push_back(tlsNode); + Trace("pp-llm") << "Learned literal : " << tlsNode << " from " << lit + << std::endl; + } + return currLearnedLits; +} + +} // namespace preprocessing +} // namespace cvc5 diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h new file mode 100644 index 000000000..2b0273628 --- /dev/null +++ b/src/preprocessing/learned_literal_manager.h @@ -0,0 +1,71 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Learned literal manager + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H +#define CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H + +#include "context/cdhashset.h" +#include "expr/node.h" +#include "theory/trust_substitutions.h" + +namespace cvc5 { +namespace preprocessing { + +/** + * This class maintains the list of learned literals that have been inferred + * during preprocessing but we have not fully processed e.g. via substitutions. + * + * In particular, notice that if an equality (= x t) is learned at top level, + * we may add x -> t to top level substitutions if t does not contain x; we can + * henceforth forget that (= x t) is a learned literal. On the other hand, if + * a literal like (> x t) is learned at top-level, it may be useful to remember + * this information. This class is concerned with the latter kind of literals. + */ +class LearnedLiteralManager +{ + public: + LearnedLiteralManager(theory::TrustSubstitutionMap& tls, + context::UserContext* u, + ProofNodeManager* pnm); + /** + * Notify learned literal. This method is called when a literal is + * entailed by the current set of assertions. + * + * It should be rewritten, and such that top level substitutions have + * been applied to it. + */ + void notifyLearnedLiteral(TNode lit); + /** + * Get learned literals, which returns the current set of learned literals + * provided to this class. These literals are refreshed so that the current + * top-level substitutions are applied to them, and then are rewritten. + */ + std::vector<Node> getLearnedLiterals() const; + + private: + /** Learned literal map */ + typedef context::CDHashSet<Node> NodeSet; + /* The top level substitutions */ + theory::TrustSubstitutionMap& d_topLevelSubs; + /** Learned literals */ + NodeSet d_learnedLits; +}; + +} // namespace preprocessing +} // namespace cvc5 + +#endif /* CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H */ diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index b6f53f8c2..ad2707035 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -408,6 +408,14 @@ Node BVToInt::translateWithChildren(Node original, returnNode = translated_children[0]; break; } + case kind::INT_TO_BITVECTOR: + { + // ((_ int2bv n) t) ---> (mod t 2^n) + size_t sz = original.getOperator().getConst<IntToBitVector>().d_size; + returnNode = d_nm->mkNode( + kind::INTS_MODULUS_TOTAL, translated_children[0], pow2(sz)); + } + break; case kind::BITVECTOR_AND: { // We support three configurations: diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 7f03b9459..15a16888d 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -69,7 +69,8 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) } else if (current.getNumChildren() > 2 && (current.getKind() == kind::PLUS - || current.getKind() == kind::MULT)) + || current.getKind() == kind::MULT + || current.getKind() == kind::NONLINEAR_MULT)) { Assert(cache.find(current[0]) != cache.end()); result = cache[current[0]]; @@ -118,15 +119,15 @@ Node intToBV(TNode n, NodeMap& cache) { // Not a leaf vector<Node> children; - unsigned max = 0; - for (unsigned i = 0; i < current.getNumChildren(); ++i) + uint64_t max = 0; + for (const Node& nc : current) { - Assert(cache.find(current[i]) != cache.end()); - TNode childRes = cache[current[i]]; + Assert(cache.find(nc) != cache.end()); + TNode childRes = cache[nc]; TypeNode type = childRes.getType(); if (type.isBitVector()) { - unsigned bvsize = type.getBitVectorSize(); + uint32_t bvsize = type.getBitVectorSize(); if (bvsize > max) { max = bvsize; @@ -146,6 +147,7 @@ Node intToBV(TNode n, NodeMap& cache) max = max + 1; break; case kind::MULT: + case kind::NONLINEAR_MULT: Assert(children.size() == 2); newKind = kind::BITVECTOR_MULT; max = max * 2; @@ -174,14 +176,14 @@ Node intToBV(TNode n, NodeMap& cache) } break; } - for (unsigned i = 0; i < children.size(); ++i) + for (size_t i = 0, csize = children.size(); i < csize; ++i) { TypeNode type = children[i].getType(); if (!type.isBitVector()) { continue; } - unsigned bvsize = type.getBitVectorSize(); + uint32_t bvsize = type.getBitVectorSize(); if (bvsize < max) { // sign extend @@ -195,10 +197,7 @@ Node intToBV(TNode n, NodeMap& cache) if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } - for (unsigned i = 0; i < children.size(); ++i) - { - builder << children[i]; - } + builder.append(children); // Mark the substitution and continue Node result = builder; @@ -226,7 +225,6 @@ Node intToBV(TNode n, NodeMap& cache) { Rational constant = current.getConst<Rational>(); if (constant.isIntegral()) { - AlwaysAssert(constant >= 0); BitVector bv(size, constant.getNumerator()); if (bv.toSignedInteger() != constant.getNumerator()) { diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index b05dbbe1c..5610b0117 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -249,6 +249,10 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { // Keep the literal learned_literals[j++] = learned_literals[i]; + // Its a literal that could not be processed as a substitution or + // conflict. In this case, we notify the context of the learned + // literal, which will process it with the learned literal manager. + d_preprocContext->notifyLearnedLiteral(learnedLiteral); } break; } diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index eaccce1a9..b21fcb261 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -30,6 +30,9 @@ PreprocessingPassContext::PreprocessingPassContext( : d_smt(smt), d_env(env), d_circuitPropagator(circuitPropagator), + d_llm(env.getTopLevelSubstitutions(), + env.getUserContext(), + env.getProofNodeManager()), d_symsInAssertions(env.getUserContext()) { } @@ -67,6 +70,16 @@ void PreprocessingPassContext::recordSymbolsInAssertions( } } +void PreprocessingPassContext::notifyLearnedLiteral(TNode lit) +{ + d_llm.notifyLearnedLiteral(lit); +} + +std::vector<Node> PreprocessingPassContext::getLearnedLiterals() +{ + return d_llm.getLearnedLiterals(); +} + void PreprocessingPassContext::addSubstitution(const Node& lhs, const Node& rhs, ProofGenerator* pg) diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 722c82f6b..1af73e453 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -23,8 +23,8 @@ #define CVC5__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H #include "context/cdhashset.h" +#include "preprocessing/learned_literal_manager.h" #include "smt/smt_engine.h" -#include "theory/trust_substitutions.h" #include "util/resource_manager.h" namespace cvc5 { @@ -75,6 +75,18 @@ class PreprocessingPassContext void recordSymbolsInAssertions(const std::vector<Node>& assertions); /** + * Notify learned literal. This method is called when a literal is + * entailed by the current set of assertions. + * + * It should be rewritten, and such that top level substitutions have + * been applied to it. + */ + void notifyLearnedLiteral(TNode lit); + /** + * Get the learned literals + */ + std::vector<Node> getLearnedLiterals(); + /** * Add substitution to the top-level substitutions, which also as a * consequence is used by the theory model. * @param lhs The node replaced by node 'rhs' @@ -101,6 +113,11 @@ class PreprocessingPassContext /** Instance of the circuit propagator */ theory::booleans::CircuitPropagator* d_circuitPropagator; /** + * The learned literal manager + */ + LearnedLiteralManager d_llm; + + /** * The (user-context-dependent) set of symbols that occur in at least one * assertion in the current user context. */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 426f60a60..076093bce 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -951,10 +951,43 @@ void Smt2Printer::toStream(std::ostream& out, return; break; } - case kind::APPLY_TESTER: case kind::APPLY_SELECTOR: - case kind::APPLY_SELECTOR_TOTAL: + { + Node op = n.getOperator(); + const DType& dt = DType::datatypeOf(op); + if (dt.isTuple()) + { + stillNeedToPrintParams = false; + out << "(_ tupSel " << DType::indexOf(op) << ") "; + } + } + break; + case kind::APPLY_TESTER: + { + stillNeedToPrintParams = false; + Node op = n.getOperator(); + size_t cindex = DType::indexOf(op); + const DType& dt = DType::datatypeOf(op); + out << "(_ is "; + toStream( + out, dt[cindex].getConstructor(), toDepth < 0 ? toDepth : toDepth - 1); + out << ") "; + } + break; case kind::APPLY_UPDATER: + { + Node op = n.getOperator(); + size_t index = DType::indexOf(op); + const DType& dt = DType::datatypeOf(op); + size_t cindex = DType::cindexOf(op); + out << "(_ update "; + toStream(out, + dt[cindex][index].getSelector(), + toDepth < 0 ? toDepth : toDepth - 1); + out << ") "; + } + break; + case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; // separation logic @@ -1037,19 +1070,8 @@ void Smt2Printer::toStream(std::ostream& out, if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { if(toDepth != 0) { - if (n.getKind() == kind::APPLY_TESTER) - { - unsigned cindex = DType::indexOf(n.getOperator()); - const DType& dt = DType::datatypeOf(n.getOperator()); - out << "(_ is "; - toStream(out, - dt[cindex].getConstructor(), - toDepth < 0 ? toDepth : toDepth - 1); - out << ")"; - }else{ - toStream( - out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); - } + toStream( + out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); } else { out << "(...)"; } diff --git a/src/smt/command.cpp b/src/smt/command.cpp index bf7d5ef3d..d672b79a6 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -31,6 +31,7 @@ #include "expr/symbol_manager.h" #include "expr/type_node.h" #include "options/options.h" +#include "options/printer_options.h" #include "options/smt_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" @@ -1403,11 +1404,16 @@ void DefineFunctionCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { + TypeNode rangeType = termToNode(d_func).getType(); + if (rangeType.isFunction()) + { + rangeType = rangeType.getRangeType(); + } Printer::getPrinter(language)->toStreamCmdDefineFunction( out, d_func.toString(), termVectorToNodes(d_formals), - termToNode(d_func).getType().getRangeType(), + rangeType, termToNode(d_formula)); } @@ -2041,6 +2047,16 @@ void GetProofCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {} +bool GetInstantiationsCommand::isEnabled(api::Solver* solver, + const api::Result& res) +{ + return (solver->getOptions().printer.instFormatMode + != options::InstFormatMode::SZS + && (res.isSat() + || (res.isSatUnknown() + && res.getUnknownExplanation() == api::Result::INCOMPLETE))) + || res.isUnsat() || res.isEntailed(); +} void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm) { try diff --git a/src/smt/command.h b/src/smt/command.h index 21ecd1964..2d32062e2 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1077,6 +1077,7 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command public: GetInstantiationsCommand(); + static bool isEnabled(api::Solver* solver, const api::Result& res); void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 1381ef87c..b6cdfb67b 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -43,6 +43,7 @@ Env::Env(NodeManager* nm, Options* opts) d_logic(), d_statisticsRegistry(std::make_unique<StatisticsRegistry>()), d_options(), + d_originalOptions(opts), d_resourceManager() { if (opts != nullptr) @@ -97,6 +98,8 @@ StatisticsRegistry& Env::getStatisticsRegistry() const Options& Env::getOptions() const { return d_options; } +const Options& Env::getOriginalOptions() const { return *d_originalOptions; } + ResourceManager* Env::getResourceManager() const { return d_resourceManager.get(); diff --git a/src/smt/env.h b/src/smt/env.h index 29a360209..57b5ad9c7 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -94,6 +94,9 @@ class Env /** Get the options object (const version only) owned by this Env. */ const Options& getOptions() const; + /** Get the original options object (const version only). */ + const Options& getOriginalOptions() const; + /** Get the resource manager owned by this Env. */ ResourceManager* getResourceManager() const; @@ -180,6 +183,12 @@ class Env * consider during solving and initialization. */ Options d_options; + /** + * A pointer to the original options object as stored in the api::Solver. + * The referenced objects holds the options as initially parsed before being + * changed, e.g., by setDefaults(). + */ + const Options* d_originalOptions; /** Manager for limiting time and abstract resource usage. */ std::unique_ptr<ResourceManager> d_resourceManager; }; /* class Env */ diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index ffc49710a..e85ea82ef 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -15,6 +15,8 @@ #include "smt/optimization_solver.h" +#include "context/cdhashmap.h" +#include "context/cdlist.h" #include "omt/omt_optimizer.h" #include "options/smt_options.h" #include "smt/assertions.h" @@ -29,7 +31,7 @@ namespace smt { OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), d_optChecker(), - d_objectives(), + d_objectives(parent->getUserContext()), d_results(), d_objectiveCombination(LEXICOGRAPHIC) { @@ -37,10 +39,14 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent) OptimizationResult::ResultType OptimizationSolver::checkOpt() { + // if the results of the previous call have different size than the + // objectives, then we should clear the pareto optimization context + if (d_results.size() != d_objectives.size()) d_optChecker.reset(); + // initialize the result vector + d_results.clear(); for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { - // reset the optimization results - d_results[i] = OptimizationResult(); + d_results.emplace_back(); } switch (d_objectiveCombination) { @@ -66,14 +72,6 @@ void OptimizationSolver::addObjective(TNode target, } d_optChecker.reset(); d_objectives.emplace_back(target, type, bvSigned); - d_results.emplace_back(OptimizationResult::UNKNOWN, Node()); -} - -void OptimizationSolver::resetObjectives() -{ - d_optChecker.reset(); - d_objectives.clear(); - d_results.clear(); } std::vector<OptimizationResult> OptimizationSolver::getValues() diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 64591d8f1..6d138deb2 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -18,6 +18,8 @@ #ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H #define CVC5__SMT__OPTIMIZATION_SOLVER_H +#include "context/cdhashmap_forward.h" +#include "context/cdlist.h" #include "expr/node.h" #include "expr/type_node.h" #include "util/result.h" @@ -74,14 +76,14 @@ class OptimizationResult * @return an enum showing whether the result is optimal, unbounded, * unsat or unknown. **/ - ResultType getType() { return d_type; } + ResultType getType() const { return d_type; } /** * Returns the optimal value. * @return Node containing the optimal value, * if getType() is not OPTIMAL, it might return an empty node or a node * containing non-optimal value **/ - Node getValue() { return d_value; } + Node getValue() const { return d_value; } private: /** the indicating whether the result is optimal or something else **/ @@ -124,13 +126,13 @@ class OptimizationObjective ~OptimizationObjective() = default; /** A getter for d_type **/ - ObjectiveType getType() { return d_type; } + ObjectiveType getType() const { return d_type; } /** A getter for d_target **/ - Node getTarget() { return d_target; } + Node getTarget() const { return d_target; } /** A getter for d_bvSigned **/ - bool bvIsSigned() { return d_bvSigned; } + bool bvIsSigned() const { return d_bvSigned; } private: /** @@ -173,7 +175,7 @@ class OptimizationSolver * * Lexicographic: optimize the objectives one-by-one, in the order they are * added: - * v_x = max(x) s.t. phi(x, y) = sat + * v_x = max(x) s.t. phi(x, y) = sat * v_y = max(y) s.t. phi(v_x, y) = sat * * Pareto: optimize multiple goals to a state such that @@ -215,11 +217,6 @@ class OptimizationSolver bool bvSigned = false); /** - * Clear all the added optimization objectives - **/ - void resetObjectives(); - - /** * Returns the values of the optimized objective after checkOpt is called * @return a vector of Optimization Result, * each containing the outcome and the value. @@ -293,7 +290,7 @@ class OptimizationSolver std::unique_ptr<SmtEngine> d_optChecker; /** The objectives to optimize for **/ - std::vector<OptimizationObjective> d_objectives; + context::CDList<OptimizationObjective> d_objectives; /** The results of the optimizations from the last checkOpt call **/ std::vector<OptimizationResult> d_results; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c245fa769..e3bbb6c5c 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -173,15 +173,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } - /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers - * we need to eagerly eliminate the operators. */ - if (options::bvSolver() == options::BVSolver::SIMPLE - || options::bvSolver() == options::BVSolver::BITBLAST) - { - opts.bv.bvLazyReduceExtf = false; - opts.bv.bvLazyRewriteExtf = false; - } - /* Disable bit-level propagation by default for the BITBLAST solver. */ if (options::bvSolver() == options::BVSolver::BITBLAST) { @@ -1420,22 +1411,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.arrays.arraysOptimizeLinear = false; } - if (!options::bitvectorEqualitySolver()) - { - if (options::bvLazyRewriteExtf()) - { - if (opts.bv.bvLazyRewriteExtfWasSetByUser) - { - throw OptionException( - "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set"); - } - } - Trace("smt") - << "disabling bvLazyRewriteExtf since equality solver is disabled" - << std::endl; - opts.bv.bvLazyRewriteExtf = false; - } - if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " diff --git a/src/theory/arith/nl/cad/lazard_evaluation.cpp b/src/theory/arith/nl/cad/lazard_evaluation.cpp new file mode 100644 index 000000000..82b127ed0 --- /dev/null +++ b/src/theory/arith/nl/cad/lazard_evaluation.cpp @@ -0,0 +1,46 @@ +#include "theory/arith/nl/cad/lazard_evaluation.h" + +#include "base/check.h" +#include "base/output.h" + +namespace cvc5::theory::arith::nl::cad { + +/** + * Do a very simple wrapper around the regular poly::infeasible_regions. + * Warn the user about doing this. + * This allows for a graceful fallback (albeit with a warning) if CoCoA is not + * available. + */ +struct LazardEvaluationState +{ + poly::Assignment d_assignment; +}; +LazardEvaluation::LazardEvaluation() + : d_state(std::make_unique<LazardEvaluationState>()) +{ +} +LazardEvaluation::~LazardEvaluation() {} + +void LazardEvaluation::add(const poly::Variable& var, const poly::Value& val) +{ + d_state->d_assignment.set(var, val); +} + +void LazardEvaluation::addFreeVariable(const poly::Variable& var) {} + +std::vector<poly::Polynomial> LazardEvaluation::reducePolynomial( + const poly::Polynomial& p) const +{ + return {p}; +} +std::vector<poly::Interval> LazardEvaluation::infeasibleRegions( + const poly::Polynomial& q, poly::SignCondition sc) const +{ + WarningOnce() + << "CAD::LazardEvaluation is disabled because CoCoA is not available. " + "Falling back to regular calculation of infeasible regions." + << std::endl; + return poly::infeasible_regions(q, d_state->d_assignment, sc); +} + +} // namespace cvc5::theory::arith::nl::cad diff --git a/src/theory/arith/nl/cad/lazard_evaluation.h b/src/theory/arith/nl/cad/lazard_evaluation.h new file mode 100644 index 000000000..0edb12010 --- /dev/null +++ b/src/theory/arith/nl/cad/lazard_evaluation.h @@ -0,0 +1,109 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implements the CDCAC approach as described in + * https://arxiv.org/pdf/2003.05633.pdf. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H +#define CVC5__THEORY__ARITH__NL__CAD__LAZARD_EVALUATION_H + +#include <poly/polyxx.h> + +#include <memory> + +namespace cvc5::theory::arith::nl::cad { + +struct LazardEvaluationState; +/** + * This class does the heavy lifting for the modified lifting procedure that is + * required for Lazard's projection. + * + * Let p \in Q[x_0, ..., x_n] a multivariate polynomial whose roots we want to + * isolate over the partial sample point A = [x_0 = a_0, ... x_{n-1} = a_{n-1}] + * where a_0, ... a_{n-1} are real algebraic numbers and x_n is the last free + * variable. + * + * The modified lifting procedure conceptually works as follows: + * + * for (x = a) in A: + * while p[x // a] = 0: + * p = p / (x - a) + * p = p[x // a] + * return roots(p) + * + * As the assignment contains real algebraic numbers, though, we can not do any + * of the computations directly, as our polynomials only support coefficients + * from Z or Q, but not extensions (in the algebraic sense) thereof. + * + * Our approach is as follows: + * Let pk be the minimal polynomial for a_k. + * Instead of substituting p[x_k // a_k] we (canonically) embed p into the + * quotient ring Q[x_k]/<p_k> and recursively build a tower of such quotient + * rings that is isomorphic to nesting the corresponding field extensions + * Q(a_1)(a_2)... When we have done that, we obtain p that is reduced with + * respect to all minimal polynomials, but may still contain x_0,... x_{n-1}. To + * get rid of these, we compute a Gröbner basis of p and the minimal polynomials + * (using a suitable elimination order) and extract the polynomial in x_n. This + * polynomial has all roots (and possibly some more) that we are looking for. + * Instead of a Gröbner basis, we can also compute the iterated resultant as + * follows: Res(Res(p, p_{n-1}, x_{n-1}), p_{n-2}, x_{n-2})... + * + * Consider + * http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2020/2020-04.pdf + * Section 2.5.1 for a full discussion. + * + * !!! WARNING !!! + * If CoCoALib is not available, this class will simply fall back to + * poly::infeasible_regions and issue a warning about this. + */ +class LazardEvaluation +{ + public: + LazardEvaluation(); + ~LazardEvaluation(); + + /** + * Add the next assigned variable x_k = a_k to this construction. + */ + void add(const poly::Variable& var, const poly::Value& val); + /** + * Finish by adding the free variable x_n. + */ + void addFreeVariable(const poly::Variable& var); + /** + * Reduce the polynomial q. Compared to the above description, there may + * actually be multiple polynomials in the Gröbner basis and instead of + * loosing this knowledge and returning their product, we return them as a + * vector. + */ + std::vector<poly::Polynomial> reducePolynomial( + const poly::Polynomial& q) const; + + /** + * Compute the infeasible regions of q under the given sign condition. + * Uses reducePolynomial and then performs real root isolation on the + * resulting polynomials to obtain the intervals. Mimics + * poly::infeasible_regions, but uses Lazard's evaluation. + */ + std::vector<poly::Interval> infeasibleRegions(const poly::Polynomial& q, + poly::SignCondition sc) const; + + private: + std::unique_ptr<LazardEvaluationState> d_state; +}; + +} // namespace cvc5::theory::arith::nl::cad + +#endif
\ No newline at end of file diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index a5c63522d..8f6d9d3b7 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -345,16 +345,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { << n << ": " << n[0].notNode() << std::endl; return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); } - if (n[1] == tt || n[1] == ff) - { - // ITE C true y --> C v y - // ITE C false y --> ~C ^ y - Node resp = - n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]); - Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const " - << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } } if (n[0].getKind() == kind::NOT) @@ -364,17 +354,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { REWRITE_AGAIN, nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1])); } - if (n[2].isConst() && (n[2] == tt || n[2] == ff)) - { - // ITE C x true --> ~C v x - // ITE C x false --> C ^ x - Node resp = - n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]); - Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const " - << n << ": " << resp << std::endl; - return RewriteResponse(REWRITE_AGAIN, resp); - } - int parityTmp; if ((parityTmp = equalityParity(n[1], n[2])) != 0) { Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]); @@ -424,6 +403,32 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); } + + // Rewrites for ITEs with a constant branch. These rewrites are applied + // after the parity rewrites above because they may simplify ITEs such as + // `(ite c c true)` to `(ite c true true)`. As a result, we avoid + // introducing an unnecessary conjunction/disjunction here. + if (n[1].isConst() && (n[1] == tt || n[1] == ff)) + { + // ITE C true y --> C v y + // ITE C false y --> ~C ^ y + Node resp = + n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]); + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + else if (n[2].isConst() && (n[2] == tt || n[2] == ff)) + { + // ITE C x true --> ~C v x + // ITE C x false --> C ^ x + Node resp = + n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]); + Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const " + << n << ": " << resp << std::endl; + return RewriteResponse(REWRITE_AGAIN, resp); + } + break; } default: diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index fbd910bee..5210117b8 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -233,18 +233,6 @@ void BVSolverLazy::check(Theory::Effort e) return; } - // last call : do reductions on extended bitvector functions - if (e == Theory::EFFORT_LAST_CALL) - { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - // check extended functions at last call effort - core->checkExtf(e); - } - return; - } - Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl; TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer); // we may be getting new assertions so the model cache may not be sound @@ -331,27 +319,6 @@ void BVSolverLazy::check(Theory::Effort e) break; } } - - // check extended functions - if (Theory::fullEffort(e)) - { - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - // check extended functions at full effort - core->checkExtf(e); - } - } -} - -bool BVSolverLazy::needsCheckLastEffort() -{ - CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE]; - if (core) - { - return core->needsCheckLastEffort(); - } - return false; } bool BVSolverLazy::collectModelValues(TheoryModel* m, diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 9b3a2f1fa..4f73354bc 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -82,8 +82,6 @@ class BVSolverLazy : public BVSolver bool preCheck(Theory::Effort e) override; - bool needsCheckLastEffort() override; - void propagate(Theory::Effort e) override; TrustNode explain(TNode n) override; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 2589418cc..fa71641ad 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -32,64 +32,6 @@ using namespace cvc5::theory; using namespace cvc5::theory::bv; using namespace cvc5::theory::bv::utils; -bool CoreSolverExtTheoryCallback::getCurrentSubstitution( - int effort, - const std::vector<Node>& vars, - std::vector<Node>& subs, - std::map<Node, std::vector<Node> >& exp) -{ - if (d_equalityEngine == nullptr) - { - return false; - } - // get the constant equivalence classes - bool retVal = false; - for (const Node& n : vars) - { - if (d_equalityEngine->hasTerm(n)) - { - Node nr = d_equalityEngine->getRepresentative(n); - if (nr.isConst()) - { - subs.push_back(nr); - exp[n].push_back(n.eqNode(nr)); - retVal = true; - } - else - { - subs.push_back(n); - } - } - else - { - subs.push_back(n); - } - } - // return true if the substitution is non-trivial - return retVal; -} - -bool CoreSolverExtTheoryCallback::getReduction(int effort, - Node n, - Node& nr, - bool& satDep) -{ - Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl; - if (n.getKind() == kind::BITVECTOR_TO_NAT) - { - nr = utils::eliminateBv2Nat(n); - satDep = false; - return true; - } - else if (n.getKind() == kind::INT_TO_BITVECTOR) - { - nr = utils::eliminateInt2Bv(n); - satDep = false; - return true; - } - return false; -} - CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv) : SubtheorySolver(c, bv), d_notify(*this), @@ -98,18 +40,8 @@ CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv) d_preregisterCalled(false), d_checkCalled(false), d_bv(bv), - d_extTheoryCb(), - d_extTheory(new ExtTheory(d_extTheoryCb, - bv->d_bv.getSatContext(), - bv->d_bv.getUserContext(), - bv->d_bv.getOutputChannel())), - d_reasons(c), - d_needsLastCallCheck(false), - d_extf_range_infer(bv->d_bv.getUserContext()), - d_extf_collapse_infer(bv->d_bv.getUserContext()) + d_reasons(c) { - d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT); - d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR); } CoreSolver::~CoreSolver() {} @@ -167,11 +99,6 @@ void CoreSolver::preRegister(TNode node) { d_equalityEngine->addTriggerPredicate(node); } else { d_equalityEngine->addTerm(node); - // Register with the extended theory, for context-dependent simplification. - // Notice we do this for registered terms but not internally generated - // equivalence classes. The two should roughly cooincide. Since ExtTheory is - // being used as a heuristic, it is good enough to be registered here. - d_extTheory->registerTerm(node); } } @@ -489,142 +416,3 @@ CoreSolver::Statistics::Statistics() "theory::bv::CoreSolver::NumCallsToCheck")) { } - -void CoreSolver::checkExtf(Theory::Effort e) -{ - if (e == Theory::EFFORT_LAST_CALL) - { - std::vector<Node> nred = d_extTheory->getActive(); - doExtfReductions(nred); - } - Assert(e == Theory::EFFORT_FULL); - // do inferences (adds external lemmas) TODO: this can be improved to add - // internal inferences - std::vector<Node> nred; - if (d_extTheory->doInferences(0, nred)) - { - return; - } - d_needsLastCallCheck = false; - if (!nred.empty()) - { - // other inferences involving bv2nat, int2bv - if (options::bvAlgExtf()) - { - if (doExtfInferences(nred)) - { - return; - } - } - if (!options::bvLazyReduceExtf()) - { - if (doExtfReductions(nred)) - { - return; - } - } - else - { - d_needsLastCallCheck = true; - } - } -} - -bool CoreSolver::needsCheckLastEffort() const { return d_needsLastCallCheck; } - -bool CoreSolver::doExtfInferences(std::vector<Node>& terms) -{ - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - bool sentLemma = false; - eq::EqualityEngine* ee = d_equalityEngine; - std::map<Node, Node> op_map; - for (unsigned j = 0; j < terms.size(); j++) - { - TNode n = terms[j]; - Assert(n.getKind() == kind::BITVECTOR_TO_NAT - || n.getKind() == kind::INT_TO_BITVECTOR); - if (n.getKind() == kind::BITVECTOR_TO_NAT) - { - // range lemmas - if (d_extf_range_infer.find(n) == d_extf_range_infer.end()) - { - d_extf_range_infer.insert(n); - unsigned bvs = n[0].getType().getBitVectorSize(); - Node min = nm->mkConst(Rational(0)); - Node max = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); - Node lem = nm->mkNode(kind::AND, - nm->mkNode(kind::GEQ, n, min), - nm->mkNode(kind::LT, n, max)); - Trace("bv-extf-lemma") - << "BV extf lemma (range) : " << lem << std::endl; - d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_LEMMA); - sentLemma = true; - } - } - Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n[0]) : n[0]; - op_map[r] = n; - } - for (unsigned j = 0; j < terms.size(); j++) - { - TNode n = terms[j]; - Node r = (ee && ee->hasTerm(n[0])) ? ee->getRepresentative(n) : n; - std::map<Node, Node>::iterator it = op_map.find(r); - if (it != op_map.end()) - { - Node parent = it->second; - // Node cterm = parent[0]==n ? parent : nm->mkNode( parent.getOperator(), - // n ); - Node cterm = parent[0].eqNode(n); - Trace("bv-extf-lemma-debug") - << "BV extf collapse based on : " << cterm << std::endl; - if (d_extf_collapse_infer.find(cterm) == d_extf_collapse_infer.end()) - { - d_extf_collapse_infer.insert(cterm); - - Node t = n[0]; - if (t.getType() == parent.getType()) - { - if (n.getKind() == kind::INT_TO_BITVECTOR) - { - Assert(t.getType().isInteger()); - // congruent modulo 2^( bv width ) - unsigned bvs = n.getType().getBitVectorSize(); - Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); - Node k = sm->mkDummySkolem( - "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence"); - t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k)); - } - Node lem = parent.eqNode(t); - - if (parent[0] != n) - { - Assert(ee->areEqual(parent[0], n)); - lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem); - } - // this handles inferences of the form, e.g.: - // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w) - // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k - Trace("bv-extf-lemma") - << "BV extf lemma (collapse) : " << lem << std::endl; - d_bv->d_im.lemma(lem, InferenceId::BV_EXTF_COLLAPSE); - sentLemma = true; - } - } - Trace("bv-extf-lemma-debug") - << "BV extf f collapse based on : " << cterm << std::endl; - } - } - return sentLemma; -} - -bool CoreSolver::doExtfReductions(std::vector<Node>& terms) -{ - std::vector<Node> nredr; - if (d_extTheory->doReductions(0, terms, nredr)) - { - return true; - } - Assert(nredr.empty()); - return false; -} diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 0dfcfdde4..46c4559ea 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -22,30 +22,11 @@ #include "context/cdhashset.h" #include "theory/bv/bv_subtheory.h" -#include "theory/ext_theory.h" namespace cvc5 { namespace theory { namespace bv { -class Base; - -/** An extended theory callback used by the core solver */ -class CoreSolverExtTheoryCallback : public ExtTheoryCallback -{ - public: - CoreSolverExtTheoryCallback() : d_equalityEngine(nullptr) {} - /** Get current substitution based on the underlying equality engine. */ - bool getCurrentSubstitution(int effort, - const std::vector<Node>& vars, - std::vector<Node>& subs, - std::map<Node, std::vector<Node> >& exp) override; - /** Get reduction. */ - bool getReduction(int effort, Node n, Node& nr, bool& satDep) override; - /** The underlying equality engine */ - eq::EqualityEngine* d_equalityEngine; -}; - /** * Bitvector equality solver */ @@ -96,10 +77,6 @@ class CoreSolver : public SubtheorySolver { BVSolverLazy* d_bv; /** Pointer to the equality engine of the parent */ eq::EqualityEngine* d_equalityEngine; - /** The extended theory callback */ - CoreSolverExtTheoryCallback d_extTheoryCb; - /** Extended theory module, for context-dependent simplification. */ - std::unique_ptr<ExtTheory> d_extTheory; /** To make sure we keep the explanations */ context::CDHashSet<Node> d_reasons; @@ -109,36 +86,6 @@ class CoreSolver : public SubtheorySolver { bool isCompleteForTerm(TNode term, TNodeBoolMap& seen); Statistics d_statistics; - /** Whether we need a last call effort check */ - bool d_needsLastCallCheck; - /** For extended functions */ - context::CDHashSet<Node> d_extf_range_infer; - context::CDHashSet<Node> d_extf_collapse_infer; - - /** do extended function inferences - * - * This method adds lemmas on the output channel of TheoryBV based on - * reasoning about extended functions, such as bv2nat and int2bv. Examples - * of lemmas added by this method include: - * 0 <= ((_ int2bv w) x) < 2^w - * ((_ int2bv w) (bv2nat x)) = x - * (bv2nat ((_ int2bv w) x)) == x + k*2^w - * The purpose of these lemmas is to recognize easy conflicts before fully - * reducing extended functions based on their full semantics. - */ - bool doExtfInferences(std::vector<Node>& terms); - /** do extended function reductions - * - * This method adds lemmas on the output channel of TheoryBV based on - * reducing all extended function applications that are preregistered to - * this theory and have not already been reduced by context-dependent - * simplification (see theory/ext_theory.h). Examples of lemmas added by - * this method include: - * (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... + - * (ite ((_ extract 1 0) x) 1 0) - */ - bool doExtfReductions(std::vector<Node>& terms); - public: CoreSolver(context::Context* c, BVSolverLazy* bv); ~CoreSolver(); @@ -154,9 +101,6 @@ class CoreSolver : public SubtheorySolver { EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool hasTerm(TNode node) const; void addTermToEqualityEngine(TNode node); - /** check extended functions at the given effort */ - void checkExtf(Theory::Effort e); - bool needsCheckLastEffort() const; }; } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 476803c59..97ca24437 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -64,7 +64,16 @@ TrustNode TheoryBVRewriter::expandDefinition(Node node) case kind::BITVECTOR_SDIV: case kind::BITVECTOR_SREM: case kind::BITVECTOR_SMOD: ret = eliminateBVSDiv(node); break; + case kind::BITVECTOR_TO_NAT: + ret = utils::eliminateBv2Nat(node); + + break; + case kind::INT_TO_BITVECTOR: + + ret = utils::eliminateInt2Bv(node); + + break; default: break; } if (!ret.isNull() && node != ret) @@ -635,8 +644,8 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){ } RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { - //do not use lazy rewrite strategy if equality solver is disabled - if( node[0].isConst() || !options::bvLazyRewriteExtf() ){ + if (node[0].isConst()) + { Node resultNode = LinearRewriteStrategy < RewriteRule<BVToNatEliminate> >::apply(node); @@ -647,8 +656,8 @@ RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { } RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) { - //do not use lazy rewrite strategy if equality solver is disabled - if( node[0].isConst() || !options::bvLazyRewriteExtf() ){ + if (node[0].isConst()) + { Node resultNode = LinearRewriteStrategy < RewriteRule<IntToBVEliminate> >::apply(node); diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b0f6e63bf..5ecc33778 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -716,7 +716,22 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl; int vo = rsi->getVariableOrder(i); Assert(q[0][vo] == d_set[q][i]); - Node t = rsi->getCurrentTerm(vo, true); + TypeNode tn = d_set[q][i].getType(); + // If the type of tn is not closed enumerable, we must map the value back + // to a term that appears in the same equivalence class as the constant. + // Notice that this is to ensure that unhandled values (e.g. uninterpreted + // constants, datatype values) do not enter instantiations/lemmas, which + // can lead to refutation unsoundness. However, it is important that we + // conversely do *not* map terms to values in other cases. In particular, + // replacing a constant c with a term t can lead to solution unsoundness + // if we are instantiating a quantified formula that corresponds to a + // reduction for t, since then the reduction is using circular reasoning: + // the current value of t is being used to reason about the range of + // its axiomatization. This is limited to reductions in the theory of + // strings, which use quantification on integers only. Note this + // impacts only quantified formulas with 2+ dimensions and dependencies + // between dimensions, e.g. str.indexof_re reduction. + Node t = rsi->getCurrentTerm(vo, !tn.isClosedEnumerable()); Trace("bound-int-rsi") << "term : " << t << std::endl; vars.push_back( d_set[q][i] ); subs.push_back( t ); diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index d0eee1886..f6af5b680 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -429,14 +429,17 @@ Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const << d_domain_elements[i].size() << std::endl; Assert(0 <= curr && curr < d_domain_elements[i].size()); Node t = d_domain_elements[i][curr]; + Trace("rsi-debug") << "rsi : term = " << t << std::endl; if (valTerm) { Node tt = d_rs->getTermForRepresentative(t); if (!tt.isNull()) { + Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl; return tt; } } + Trace("rsi-debug") << "rsi : return" << std::endl; return t; } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 152a3e180..dbb6d4cf3 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -163,8 +163,9 @@ Node StringsPreprocess::reduce(Node t, Node a2 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, sk3, sk2)); // length of first skolem is second argument Node a3 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); + Node a4 = nm->mkNode(STRING_LENGTH, rs).eqNode(nm->mkNode(STRING_LENGTH, sk3)); - Node b1 = nm->mkNode(AND, a1, a2, a3); + Node b1 = nm->mkNode(AND, {a1, a2, a3, a4}); Node b2 = skt.eqNode(s); Node lemma = nm->mkNode(ITE, cond, b1, b2); @@ -172,7 +173,8 @@ Node StringsPreprocess::reduce(Node t, // IF n >=0 AND n < len( s ) // THEN: skt = sk1 ++ substr(r,0,len(s)-n) ++ sk2 AND // s = sk1 ++ sk3 ++ sk2 AND - // len( sk1 ) = n + // len( sk1 ) = n AND + // len( substr(r,0,len(s)-n) ) = len( sk3 ) // ELSE: skt = s // We use an optimization where r is used instead of substr(r,0,len(s)-n) // if r is a constant of length one. @@ -321,7 +323,7 @@ Node StringsPreprocess::reduce(Node t, // n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i => // ~in_re(substr(s, i, l), r)) ^ // (skk != -1 => - // exists l. 0 <= l < len(s) - skk ^ in_re(substr(s, skk, l), r)) + // exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s, skk, l), r)) // // Note that this reduction relies on eager reduction lemmas being sent to // properly limit the range of skk. diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1afb8cc31..36b05b145 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -148,56 +148,54 @@ void TheoryUF::postCheck(Effort level) } } -bool TheoryUF::preNotifyFact( - TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) +void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) { + if (d_state.isInConflict()) + { + return; + } if (d_thss != nullptr) { bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); d_thss->assertNode(fact, isDecision); - if (d_state.isInConflict()) - { - return true; - } } - if (atom.getKind() == kind::CARDINALITY_CONSTRAINT - || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) + switch (atom.getKind()) { - if (d_thss == nullptr) + case kind::EQUAL: { - if (!getLogicInfo().hasCardinalityConstraints()) + if (options::ufHo() && options::ufHoExt()) { - std::stringstream ss; - ss << "Cardinality constraint " << atom - << " was asserted, but the logic does not allow it." << std::endl; - ss << "Try using a logic containing \"UFC\"." << std::endl; - throw Exception(ss.str()); - } - else - { - // support for cardinality constraints is not enabled, set incomplete - d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); + if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) + { + // apply extensionality eagerly using the ho extension + d_ho->applyExtensionality(fact); + } } } - // don't need to assert cardinality constraints if not producing models - return !options::produceModels(); - } - return false; -} - -void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) -{ - if (!d_state.isInConflict() && atom.getKind() == kind::EQUAL) - { - if (options::ufHo() && options::ufHoExt()) + break; + case kind::CARDINALITY_CONSTRAINT: + case kind::COMBINED_CARDINALITY_CONSTRAINT: { - if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) + if (d_thss == nullptr) { - // apply extensionality eagerly using the ho extension - d_ho->applyExtensionality(fact); + if (!getLogicInfo().hasCardinalityConstraints()) + { + std::stringstream ss; + ss << "Cardinality constraint " << atom + << " was asserted, but the logic does not allow it." << std::endl; + ss << "Try using a logic containing \"UFC\"." << std::endl; + throw Exception(ss.str()); + } + else + { + // support for cardinality constraints is not enabled, set incomplete + d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); + } } } + break; + default: break; } } //--------------------------------- end standard check diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index c811e08e8..c953cfe5c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -128,12 +128,6 @@ private: bool needsCheckLastEffort() override; /** Post-check, called after the fact queue of the theory is processed. */ void postCheck(Effort level) override; - /** Pre-notify fact, return true if processed. */ - bool preNotifyFact(TNode atom, - bool pol, - TNode fact, - bool isPrereg, - bool isInternal) override; /** Notify fact */ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; //--------------------------------- end standard check diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py index 32813e17f..e78188079 100644 --- a/test/python/unit/api/test_term.py +++ b/test/python/unit/api/test_term.py @@ -15,6 +15,7 @@ import pytest import pycvc5 from pycvc5 import kinds from pycvc5 import Sort, Term +from fractions import Fraction @pytest.fixture @@ -1145,12 +1146,27 @@ def test_get_real(solver): assert 0 == real1.getRealValue() assert 0 == real2.getRealValue() assert -17 == real3.getRealValue() - assert -3 / 5 == real4.getRealValue() - assert 127 / 10 == real5.getRealValue() - assert 1 / 4294967297 == real6.getRealValue() + assert Fraction(-3, 5) == real4.getRealValue() + assert Fraction(127, 10) == real5.getRealValue() + assert Fraction(1, 4294967297) == real6.getRealValue() assert 4294967297 == real7.getRealValue() - assert 1 / 18446744073709551617 == real8.getRealValue() - assert float(18446744073709551617) == real9.getRealValue() + assert Fraction(1, 18446744073709551617) == real8.getRealValue() + assert Fraction(18446744073709551617, 1) == real9.getRealValue() + + # Check denominator too large for float + num = 1 + den = 2 ** 64 + 1 + real_big = solver.mkReal(num, den) + assert real_big.isRealValue() + assert Fraction(num, den) == real_big.getRealValue() + + # Check that we're treating floats as decimal aproximations rather than + # IEEE-754-specified values. + real_decimal = solver.mkReal(0.3) + assert real_decimal.isRealValue() + assert Fraction("0.3") == real_decimal.getRealValue() + assert Fraction(0.3) == Fraction(5404319552844595, 18014398509481984) + assert Fraction(0.3) != real_decimal.getRealValue() def test_get_boolean(solver): diff --git a/test/python/unit/api/test_to_python_obj.py b/test/python/unit/api/test_to_python_obj.py index 2ba685d50..bb30fae8f 100644 --- a/test/python/unit/api/test_to_python_obj.py +++ b/test/python/unit/api/test_to_python_obj.py @@ -22,8 +22,8 @@ def testGetBool(): solver = pycvc5.Solver() t = solver.mkTrue() f = solver.mkFalse() - assert t.toPythonObj() == True - assert f.toPythonObj() == False + assert t.toPythonObj() is True + assert f.toPythonObj() is False def testGetInt(): @@ -115,4 +115,4 @@ def testGetValueReal(): xval = solver.getValue(x) yval = solver.getValue(y) assert xval.toPythonObj() == Fraction("6") - assert yval.toPythonObj() == float(Fraction("8.33")) + assert yval.toPythonObj() == Fraction("8.33") diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bd90627f8..1da2630af 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -163,6 +163,7 @@ set(regress_0_tests regress0/auflia/fuzz05.smtv1.smt2 regress0/auflia/x2.smtv1.smt2 regress0/bool/issue1978.smt2 + regress0/bool/issue6717-ite-rewrite.smt2 regress0/boolean-prec.cvc regress0/boolean-terms-bug-array.smt2 regress0/boolean-terms-kernel1.smt2 @@ -644,6 +645,10 @@ set(regress_0_tests regress0/incorrect1.smtv1.smt2 regress0/ineq_basic.smtv1.smt2 regress0/ineq_slack.smtv1.smt2 + regress0/int-to-bv/basic.smt2 + regress0/int-to-bv/neg-consts.smt2 + regress0/int-to-bv/not-enough-bits.smt2 + regress0/int-to-bv/overflow.smt2 regress0/issue1063-overloading-dt-cons.smt2 regress0/issue1063-overloading-dt-fun.smt2 regress0/issue1063-overloading-dt-sel.smt2 @@ -737,6 +742,7 @@ set(regress_0_tests regress0/options/ast-and-sexpr.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-and-get-options.smt2 + regress0/options/statistics.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 @@ -1491,6 +1497,7 @@ set(regress_1_tests regress1/bags/union_disjoint.smt2 regress1/bags/union_max1.smt2 regress1/bags/union_max2.smt2 + regress1/bv2int-isabelle.smt2 regress1/bv/bench_38.delta.smt2 regress1/bv/bug787.smt2 regress1/bv/bug_extract_mult_leading_bit.smt2 @@ -2127,6 +2134,11 @@ set(regress_1_tests regress1/strings/issue6337-replace-re.smt2 regress1/strings/issue6567-empty-re-range.smt2 regress1/strings/issue6604-2.smt2 + regress1/strings/issue6635-rre.smt2 + regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-4-rre.smt2 + regress1/strings/issue6653-rre.smt2 + regress1/strings/issue6653-rre-small.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 b/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 new file mode 100644 index 000000000..3f78823df --- /dev/null +++ b/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(declare-fun T () Bool) +(declare-fun v () String) +(assert (ite T T true)) +(assert (or T (and (str.prefixof v "") (exists ((x Int)) (= "t" (str.substr v 0 x)))))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2 index 1f5015d14..60826da85 100644 --- a/test/regress/regress0/bv/bv-int-collapse1.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=lazy +; COMMAND-LINE: --solve-bv-as-int=sum ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2 index d56188dad..130b045d9 100644 --- a/test/regress/regress0/bv/bv-int-collapse2.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=lazy +; COMMAND-LINE: --solve-bv-as-int=sum ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2 index 31e2b7bd1..daae6a1c3 100644 --- a/test/regress/regress0/bv/bv2nat-simp-range.smt2 +++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --solve-bv-as-int=sum ; EXPECT: unsat (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/regress0/int-to-bv/basic.smt2 b/test/regress/regress0/int-to-bv/basic.smt2 new file mode 100644 index 000000000..1e30a7ee8 --- /dev/null +++ b/test/regress/regress0/int-to-bv/basic.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-int-as-bv=5 --no-check-models +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +; Tests the conversion of negative constants and non-linear multiplication +(assert (= (- 2) (* x y))) +; Operators with more than two children +(assert (= 8 (* x x x))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/int-to-bv/neg-consts.smt2 b/test/regress/regress0/int-to-bv/neg-consts.smt2 new file mode 100644 index 000000000..46c08dad5 --- /dev/null +++ b/test/regress/regress0/int-to-bv/neg-consts.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +(assert (> (- 1) x)) +(assert (>= y x)) +(assert (< 0 y)) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/int-to-bv/not-enough-bits.smt2 b/test/regress/regress0/int-to-bv/not-enough-bits.smt2 new file mode 100644 index 000000000..49711ecc9 --- /dev/null +++ b/test/regress/regress0/int-to-bv/not-enough-bits.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --solve-int-as-bv=3 +; SCRUBBER: sed -n "s/.*\(Not enough bits\).*: 4.*/\1/p" +; EXPECT: Not enough bits +; EXIT: 1 +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +; The negative constant fits, the positive does not +(assert (= (- 4) (* x y))) +(assert (= 4 (* x y))) +(check-sat) diff --git a/test/regress/regress0/int-to-bv/overflow.smt2 b/test/regress/regress0/int-to-bv/overflow.smt2 new file mode 100644 index 000000000..30e47adb3 --- /dev/null +++ b/test/regress/regress0/int-to-bv/overflow.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-int-as-bv=4 +; EXPECT: unknown +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +(assert (= (- 1) (+ x y))) +(assert (> x 0)) +(assert (> y 0)) +(check-sat) diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2 new file mode 100644 index 000000000..ae9d93b6f --- /dev/null +++ b/test/regress/regress0/options/statistics.smt2 @@ -0,0 +1,43 @@ +; REQUIRES: statistics +; EXPECT: false +; EXPECT: false +; EXPECT: false +; EXPECT: false +; EXPECT: true +; EXPECT: true +; EXPECT: false +; EXPECT: false +; EXPECT: false +; EXPECT: false +; EXPECT: false +; EXPECT: false +; EXPECT: true +; EXPECT: false +; EXPECT: false +; EXPECT: true +(set-logic QF_UF) +(get-option :stats) +(get-option :stats-all) +(get-option :stats-every-query) +(get-option :stats-expert) + +(set-option :stats-all true) + +(get-option :stats) +(get-option :stats-all) +(get-option :stats-every-query) +(get-option :stats-expert) + +(set-option :stats false) + +(get-option :stats) +(get-option :stats-all) +(get-option :stats-every-query) +(get-option :stats-expert) + +(set-option :stats-expert true) + +(get-option :stats) +(get-option :stats-all) +(get-option :stats-every-query) +(get-option :stats-expert)
\ No newline at end of file diff --git a/test/regress/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2 index 7e0da282e..b68051719 100644 --- a/test/regress/regress1/bv/bv2nat-ground.smt2 +++ b/test/regress/regress1/bv/bv2nat-ground.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=lazy +; COMMAND-LINE: --solve-bv-as-int=sum ; EXPECT: unsat (set-logic QF_BVLIA) (set-info :status unsat) diff --git a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 index 9da8d4ca8..66b286da1 100644 --- a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 +++ b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --solve-bv-as-int=sum +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun t () (_ BitVec 16)) diff --git a/test/regress/regress1/bv2int-isabelle.smt2 b/test/regress/regress1/bv2int-isabelle.smt2 new file mode 100644 index 000000000..e8d1efe51 --- /dev/null +++ b/test/regress/regress1/bv2int-isabelle.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --solve-bv-as-int=sum --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL) +(declare-fun s$ () (_ BitVec 32)) +(declare-fun x$ () (_ BitVec 32)) +(declare-fun i$ () (_ BitVec 32)) +(define-fun bound () Int (bv2nat ((_ int2bv 32) 2048))) +(define-fun bseg ((x (_ BitVec 32)) (s (_ BitVec 32))) Bool (and (< (bv2nat x) bound) (<= (+ (bv2nat x) (bv2nat s)) bound))) + +;assumptions +(assert (bseg x$ s$)) +(assert (<= (bv2nat i$) (bv2nat s$))) + +;conclusion +(assert (not (= (bv2nat (bvadd x$ i$)) (+ (bv2nat x$) (bv2nat i$))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6635-rre.smt2 b/test/regress/regress1/strings/issue6635-rre.smt2 new file mode 100644 index 000000000..cbca77783 --- /dev/null +++ b/test/regress/regress1/strings/issue6635-rre.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () String) +(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A")))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 b/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 new file mode 100644 index 000000000..88a89b725 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-2-update-c-len.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-info :status sat) +(set-option :strings-lazy-pp false) +(set-option :check-unsat-cores true) +(declare-fun s () String) +(assert (not (= "A" (str.substr (str.update "AAAAAA" 1 s) 5 1)))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-4-rre.smt2 b/test/regress/regress1/strings/issue6653-4-rre.smt2 new file mode 100644 index 000000000..8de99a334 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-4-rre.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun x () String) +(assert (str.in_re (str.replace_re x (str.to_re "A") x) (re.++ (re.comp (str.to_re "A")) (str.to_re "A") re.allchar))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-rre-small.smt2 b/test/regress/regress1/strings/issue6653-rre-small.smt2 new file mode 100644 index 000000000..c4b6a497b --- /dev/null +++ b/test/regress/regress1/strings/issue6653-rre-small.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(assert (str.in_re a (re.+ (str.to_re (str.replace_re a (str.to_re a) "A"))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-rre.smt2 b/test/regress/regress1/strings/issue6653-rre.smt2 new file mode 100644 index 000000000..66b7dd64e --- /dev/null +++ b/test/regress/regress1/strings/issue6653-rre.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(declare-fun b () String) +(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b")))) +(assert (str.in_re a (re.* (re.range "a" "b")))) +(check-sat) diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2 index c8cf40abf..165e39e7a 100644 --- a/test/regress/regress2/bv_to_int_mask_array_1.smt2 +++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum -; COMMAND-LINE: --solve-bv-as-int=bv +; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores ; EXPECT: unsat (set-logic ALL) (declare-fun A () (Array Int Int)) diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 94a2e5fb6..98fabc727 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -67,7 +67,8 @@ class TestNodeBlackNode : public TestNode char* argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-lang=ast"); - Options::parseOptions(&opts, 2, argv); + std::string progName; + Options::parseOptions(&opts, 2, argv, progName); free(argv[0]); free(argv[1]); d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts)); diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 66efe7eff..c23ce79dd 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, (uint32_t)0x3FFFFFA1)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, signed_min) @@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) // expect the minimum x = -1 ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, unsigned_max) @@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, 2u)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, signed_max) @@ -137,7 +137,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, 10u)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, min_boundary) @@ -161,7 +161,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(), BitVector(32u, 18u)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } } // namespace test diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index f16db0c0e..cf0434ddc 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), Rational("99")); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, min) @@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), Rational("1")); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, result) @@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteIntOpt, result) // We expect our check to have returned UNSAT ASSERT_EQ(r, OptimizationResult::UNSAT); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, open_interval) @@ -164,7 +164,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(), Rational("112")); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } } // namespace test diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 1950d9ae2..73c6d9e7e 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -240,5 +240,69 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.size(), 0); } +TEST_F(TestTheoryWhiteOptMultigoal, pushpop) +{ + d_smtEngine->resetAssertions(); + Node x = d_nodeManager->mkVar(*d_BV32Type); + Node y = d_nodeManager->mkVar(*d_BV32Type); + Node z = d_nodeManager->mkVar(*d_BV32Type); + + // 18 <= x + d_smtEngine->assertFormula(d_nodeManager->mkNode( + kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x)); + + // y <= x + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); + + // Lexico optimization + OptimizationSolver optSolver(d_smtEngine.get()); + + optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); + + // minimize x + optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); + + // push + d_smtEngine->push(); + + // maximize y with `signed` comparison over bit-vectors. + optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true); + // maximize z + optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); + + OptimizationResult::ResultType r = optSolver.checkOpt(); + + ASSERT_EQ(r, OptimizationResult::OPTIMAL); + + std::vector<OptimizationResult> results = optSolver.getValues(); + + // x == 18 + ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u)); + + // y == 18 + ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u)); + + // z == 0xFFFFFFFF + ASSERT_EQ(results[2].getValue().getConst<BitVector>(), + BitVector(32u, (unsigned)0xFFFFFFFF)); + + // pop + d_smtEngine->pop(); + + // now we only have one objective: (minimize x) + r = optSolver.checkOpt(); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); + results = optSolver.getValues(); + ASSERT_EQ(results.size(), 1); + ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u)); + + // resetting the assertions also resets the optimization objectives + d_smtEngine->resetAssertions(); + r = optSolver.checkOpt(); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); + results = optSolver.getValues(); + ASSERT_EQ(results.size(), 0); +} + } // namespace test } // namespace cvc5 |