diff options
30 files changed, 406 insertions, 131 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..db72b3a6b 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) @@ -140,13 +140,10 @@ QF_ABV) 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 + finishwith --bitblast=eager ;; QF_BV) - finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + finishwith --bitblast=eager --bv-assert-input ;; QF_AUFLIA) finishwith --no-arrays-eager-index --arrays-eager-lemmas --decision=justification @@ -162,8 +159,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..c6901ff5b 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -38,7 +38,7 @@ 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 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/ext/smtliblexer.py b/docs/ext/smtliblexer.py index 5dd54d006..2ce860e39 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -9,13 +9,17 @@ class SmtLibLexer(RegexLexer): 'root': [ (r'QF_BV', token.Text), (r'QF_UFDT', token.Text), - (r'ALL_SUPPORTED', token.Text), + (r'ALL', token.Text), + (r'QF_ALL', 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,6 +36,7 @@ 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'BitVec', token.Name.Attribute), (r'RNE', token.Name.Attribute), @@ -48,11 +53,15 @@ class SmtLibLexer(RegexLexer): (r'bvult', token.Operator), (r'bvule', token.Operator), (r'bvsdiv', token.Operator), + (r'emp', token.Operator), (r'extract', token.Operator), (r'fp.gt', token.Operator), (r'ite', token.Operator), (r'mkTuple', token.Operator), (r'to_fp_unsigned', token.Operator), + (r'pto', token.Operator), + (r'sep', token.Operator), + (r'wand', token.Operator), (r'\+zero', token.Operator), (r'#b[0-1]+', token.Text), (r'bv[0-9]+', token.Text), 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/theory.rst b/docs/theory.rst index 45be41b2e..f0b25aea4 100644 --- a/docs/theory.rst +++ b/docs/theory.rst @@ -5,3 +5,4 @@ Theory References :maxdepth: 1 theories/datatypes + theories/separation-logic diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index b4596e977..be9083960 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 { 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/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/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp index 5b301592a..fa6a01791 100644 --- a/src/preprocessing/learned_literal_manager.cpp +++ b/src/preprocessing/learned_literal_manager.cpp @@ -27,7 +27,7 @@ LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls, { } -void LearnedLiteralManager::notifyLearnedLiteral(Node lit) +void LearnedLiteralManager::notifyLearnedLiteral(TNode lit) { d_learnedLits.insert(lit); Trace("pp-llm") << "LLM:notifyLearnedLiteral: " << lit << std::endl; diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h index 2148b3f7c..2b0273628 100644 --- a/src/preprocessing/learned_literal_manager.h +++ b/src/preprocessing/learned_literal_manager.h @@ -48,7 +48,7 @@ class LearnedLiteralManager * It should be rewritten, and such that top level substitutions have * been applied to it. */ - void notifyLearnedLiteral(Node lit); + 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 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 04a57e0e9..1f64bd23d 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/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/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2 index 047c039ee..ae9d93b6f 100644 --- a/test/regress/regress0/options/statistics.smt2 +++ b/test/regress/regress0/options/statistics.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: statistics ; EXPECT: false ; EXPECT: false ; EXPECT: false 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 |