diff options
49 files changed, 160 insertions, 42 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index fe3dbc62b..c2374c6ff 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -130,7 +130,11 @@ bool ProcessAssertions::apply(Assertions& as) << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", assertions); - d_exDefs.expandAssertions(assertions, false); + // Expand definitions, which replaces defined functions with their definition + // and does beta reduction. Notice we pass true as the second argument since + // we do not want to call theories to expand definitions here, since we want + // to give the opportunity to rewrite/preprocess terms before expansion. + d_exDefs.expandAssertions(assertions, true); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 577407c07..142f02eab 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -25,7 +25,10 @@ ArithPreprocess::ArithPreprocess(ArithState& state, : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext()) { } -TrustNode ArithPreprocess::eliminate(TNode n) { return d_opElim.eliminate(n); } +TrustNode ArithPreprocess::eliminate(TNode n, bool partialOnly) +{ + return d_opElim.eliminate(n, partialOnly); +} bool ArithPreprocess::reduceAssertion(TNode atom) { context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it = diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index 165209bd9..622357e73 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -46,8 +46,13 @@ class ArithPreprocess * Call eliminate operators on formula n, return the resulting trust node, * which is of TrustNodeKind REWRITE and whose node is the result of * eliminating extended operators from n. + * + * @param n The node to eliminate operators from + * @param partialOnly Whether we are eliminating partial operators only. + * @return the trust node proving (= n nr) where nr is the return of + * eliminating operators in n, or the null trust node if n was unchanged. */ - TrustNode eliminate(TNode n); + TrustNode eliminate(TNode n, bool partialOnly = false); /** * Reduce assertion. This sends a lemma via the inference manager if atom * contains any extended operators. When applicable, the lemma is of the form: diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp index 4d4c4a6f5..fbd1798cd 100644 --- a/src/theory/arith/operator_elim.cpp +++ b/src/theory/arith/operator_elim.cpp @@ -46,21 +46,23 @@ void OperatorElim::checkNonLinearLogic(Node term) } } -TrustNode OperatorElim::eliminate(Node n) +TrustNode OperatorElim::eliminate(Node n, bool partialOnly) { TConvProofGenerator* tg = nullptr; - Node nn = eliminateOperators(n, tg); + Node nn = eliminateOperators(n, tg, partialOnly); if (nn != n) { // since elimination may introduce new operators to eliminate, we must // recursively eliminate result - Node nnr = eliminateOperatorsRec(nn, tg); + Node nnr = eliminateOperatorsRec(nn, tg, partialOnly); return TrustNode::mkTrustRewrite(n, nnr, nullptr); } return TrustNode::null(); } -Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg) +Node OperatorElim::eliminateOperatorsRec(Node n, + TConvProofGenerator* tg, + bool partialOnly) { Trace("arith-elim") << "Begin elim: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -108,12 +110,12 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg) { ret = nm->mkNode(cur.getKind(), children); } - Node retElim = eliminateOperators(ret, tg); + Node retElim = eliminateOperators(ret, tg, partialOnly); if (retElim != ret) { // recursively eliminate operators in result, since some eliminations // are defined in terms of other non-standard operators. - ret = eliminateOperatorsRec(retElim, tg); + ret = eliminateOperatorsRec(retElim, tg, partialOnly); } visited[cur] = ret; } @@ -123,7 +125,9 @@ Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg) return visited[n]; } -Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg) +Node OperatorElim::eliminateOperators(Node node, + TConvProofGenerator* tg, + bool partialOnly) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); @@ -143,6 +147,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg) case TO_INTEGER: case IS_INTEGER: { + if (partialOnly) + { + // not eliminating total operators + return node; + } Node toIntSkolem; std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]); if (it == d_to_int_skolem.end()) @@ -180,6 +189,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg) case INTS_DIVISION_TOTAL: case INTS_MODULUS_TOTAL: { + if (partialOnly) + { + // not eliminating total operators + return node; + } Node den = Rewriter::rewrite(node[1]); Node num = Rewriter::rewrite(node[0]); Node intVar; @@ -283,6 +297,11 @@ Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg) } case DIVISION_TOTAL: { + if (partialOnly) + { + // not eliminating total operators + return node; + } Node num = Rewriter::rewrite(node[0]); Node den = Rewriter::rewrite(node[1]); if (den.isConst()) diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h index c7b55caf1..bca80ea4d 100644 --- a/src/theory/arith/operator_elim.h +++ b/src/theory/arith/operator_elim.h @@ -37,7 +37,7 @@ class OperatorElim : public EagerProofGenerator * transcendental functions), then we replace it by a form that eliminates * that operator. This may involve the introduction of witness terms. */ - TrustNode eliminate(Node n); + TrustNode eliminate(Node n, bool partialOnly = false); /** * Get axiom for term n. This returns the axiom that this class uses to * eliminate the term n, which is determined by its top-most symbol. @@ -101,7 +101,7 @@ class OperatorElim : public EagerProofGenerator * @param n The node to eliminate operators from. * @return The (single step) eliminated form of n. */ - Node eliminateOperators(Node n, TConvProofGenerator* tg); + Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly); /** * Recursively ensure that n has no non-standard operators. This applies * the above method on all subterms of n. @@ -109,7 +109,7 @@ class OperatorElim : public EagerProofGenerator * @param n The node to eliminate operators from. * @return The eliminated form of n. */ - Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg); + Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg, bool partialOnly); /** get arithmetic skolem * * Returns the Skolem in the above map for the given id, creating it if it diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 247772897..b8cead4fc 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -97,6 +97,12 @@ void TheoryArith::preRegisterTerm(TNode n) d_internal->preRegisterTerm(n); } +TrustNode TheoryArith::expandDefinition(Node node) +{ + // call eliminate operators, to eliminate partial operators only + return d_arithPreproc.eliminate(node, true); +} + void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); } TrustNode TheoryArith::ppRewrite(TNode atom) @@ -140,8 +146,9 @@ TrustNode TheoryArith::ppRewriteTerms(TNode n) // theories may generate lemmas that involve non-standard operators. For // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may // introduce non-standard arithmetic terms appearing in grammars. - // call eliminate operators - return d_arithPreproc.eliminate(n); + // call eliminate operators. In contrast to expandDefinitions, we eliminate + // *all* extended arithmetic operators here, including total ones. + return d_arithPreproc.eliminate(n, false); } Theory::PPAssertStatus TheoryArith::ppAssert( diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e6029faef..e26ff51ef 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -68,7 +68,11 @@ class TheoryArith : public Theory { /** finish initialization */ void finishInit() override; //--------------------------------- end initialization - + /** + * Expand definition, which eliminates extended operators like div/mod in + * the given node. + */ + TrustNode expandDefinition(Node node) override; /** * Does non-context dependent setup for a node connected to a theory. */ diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3e59aebe6..4d4ec89b4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -318,6 +318,12 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck TrustNode TheoryArrays::ppRewrite(TNode term) { + // first, see if we need to expand definitions + TrustNode texp = expandDefinition(term); + if (!texp.isNull()) + { + return texp; + } if (!d_preprocess) { return TrustNode::null(); diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d43fa3927..7285b6768 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -200,7 +200,16 @@ Theory::PPAssertStatus TheoryBV::ppAssert( return d_internal->ppAssert(tin, outSubstitutions); } -TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); } +TrustNode TheoryBV::ppRewrite(TNode t) +{ + // first, see if we need to expand definitions + TrustNode texp = expandDefinition(t); + if (!texp.isNull()) + { + return texp; + } + return d_internal->ppRewrite(t); +} void TheoryBV::presolve() { d_internal->presolve(); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 74c822215..ff36216c2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -431,6 +431,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { Trace("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl; + // external selectors should be preprocessed away by now + Assert(n.getKind() != APPLY_SELECTOR); // must ensure the type is well founded and has no nested recursion if // the option dtNestedRec is not set to true. TypeNode tn = n.getType(); @@ -595,7 +597,12 @@ TrustNode TheoryDatatypes::expandDefinition(Node n) TrustNode TheoryDatatypes::ppRewrite(TNode in) { Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; - + // first, see if we need to expand definitions + TrustNode texp = expandDefinition(in); + if (!texp.isNull()) + { + return texp; + } if( in.getKind()==EQUAL ){ Node nn; std::vector< Node > rew; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 01fab92c8..ce423a7fe 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -454,6 +454,12 @@ TrustNode TheoryFp::expandDefinition(Node node) TrustNode TheoryFp::ppRewrite(TNode node) { Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl; + // first, see if we need to expand definitions + TrustNode texp = expandDefinition(node); + if (!texp.isNull()) + { + return texp; + } Node res = node; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 59666f6fd..aa847d8ea 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1612,7 +1612,10 @@ void CegInstantiator::registerCounterexampleLemma(Node lem, // already processed variable continue; } - if (ces.getType().isBoolean()) + // must avoid selector symbols, and function skolems introduced by + // theory preprocessing + TypeNode ct = ces.getType(); + if (ct.isBoolean() || ct.isFunctionLike()) { // Boolean variables, including the counterexample literal, don't matter // since they are always assigned a model value. diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 57778b4c8..615ff987a 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -126,6 +126,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) { return; } + Trace("quant-dsplit") << "QuantDSplit::check" << std::endl; NodeManager* nm = NodeManager::currentNM(); FirstOrderModel* m = d_quantEngine->getModel(); std::vector<Node> lemmas; @@ -134,6 +135,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) ++it) { Node q = it->first; + Trace("quant-dsplit") << "- Split quantifier " << q << std::endl; if (m->isQuantifierAsserted(q) && m->isQuantifierActive(q) && d_added_split.find(q) == d_added_split.end()) { @@ -196,5 +198,6 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl; d_quantEngine->addLemma(lem, false); } + Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl; } diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 0e6ab1b18..e4f281de8 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -68,6 +68,9 @@ void TheorySets::finishInit() d_valuation.setUnevaluatedKind(COMPREHENSION); // choice is used to eliminate witness d_valuation.setUnevaluatedKind(WITNESS); + // Universe set is not evaluated. This is moreover important for ensuring that + // we do not eliminate terms whose value involves the universe set. + d_valuation.setUnevaluatedKind(UNIVERSE_SET); // functions we are doing congruence over d_equalityEngine->addFunctionKind(SINGLETON); @@ -128,6 +131,11 @@ void TheorySets::preRegisterTerm(TNode node) TrustNode TheorySets::expandDefinition(Node n) { + return d_internal->expandDefinition(n); +} + +TrustNode TheorySets::ppRewrite(TNode n) +{ Kind nk = n.getKind(); if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE || nk == COMPREHENSION) @@ -150,7 +158,8 @@ TrustNode TheorySets::expandDefinition(Node n) throw LogicException(ss.str()); } } - return d_internal->expandDefinition(n); + // just expand definitions + return expandDefinition(n); } Theory::PPAssertStatus TheorySets::ppAssert( diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a5f8fa4d8..3b95c7e00 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -77,6 +77,7 @@ class TheorySets : public Theory std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; TrustNode expandDefinition(Node n) override; + TrustNode ppRewrite(TNode n) override; PPAssertStatus ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions) override; void presolve() override; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 110ff9b2d..72a4ae50d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -997,6 +997,12 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; + // first, see if we need to expand definitions + TrustNode texp = expandDefinition(atom); + if (!texp.isNull()) + { + return texp; + } TrustNode ret; Node atomRet = atom; if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index da0fc8de4..84212fa1b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1402,7 +1402,8 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, // get the node Node node = tlemma.getNode(); Node lemma = tlemma.getProven(); - Trace("te-lemma") << "Lemma, input: " << lemma << std::endl; + Trace("te-lemma") << "Lemma, input: " << lemma << ", property = " << p + << std::endl; Assert(!expr::hasFreeVar(lemma)); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 09ce71577..5298a2ca9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1689,7 +1689,6 @@ set(regress_1_tests regress1/quantifiers/smtlib46f14a.smt2 regress1/quantifiers/smtlibe99bbe.smt2 regress1/quantifiers/smtlibf957ea.smt2 - regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/symmetric_unsat_7.smt2 regress1/quantifiers/var-eq-trigger.smt2 @@ -2159,7 +2158,6 @@ set(regress_2_tests regress2/bv_to_int_5095_2.smt2 regress2/bv_to_int_ashr.smt2 regress2/bv_to_int_bitwise.smt2 - regress2/bv_to_int_bvmul1.smt2 regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 regress2/bv_to_int_inc1.smt2 regress2/bv_to_int_mask_array_1.smt2 @@ -2586,6 +2584,8 @@ set(regression_disabled_tests regress1/quantifiers/nl-pow-trick.smt2 # timeout after changes to nonlinear on PR #5351 regress1/quantifiers/rel-trigger-unusable.smt2 + # changes to expand definitions, related to trigger selection for selectors + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 @@ -2620,6 +2620,8 @@ set(regression_disabled_tests # timeout on debug regress2/arith/real2int-test.smt2 regress2/bug396.smt2 + # due to bv2int not handling unsigned/signed division + regress2/bv_to_int_bvmul1.smt2 regress2/nl/dumortier-050317.smt2 regress2/nl/nt-lemmas-bad.smt2 regress2/quantifiers/ForElimination-scala-9.smt2 diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2 index 76bc4095f..c7771d5c9 100644 --- a/test/regress/regress0/arith/div-chainable.smt2 +++ b/test/regress/regress0/arith/div-chainable.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_LIA) (set-info :status sat) diff --git a/test/regress/regress0/arith/issue3413.smt2 b/test/regress/regress0/arith/issue3413.smt2 index 290850d1a..c871226ce 100644 --- a/test/regress/regress0/arith/issue3413.smt2 +++ b/test/regress/regress0/arith/issue3413.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_NIA) (declare-fun a () Int) (declare-fun e () Int) diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2 index 3b84b7aff..e4bac6a0a 100644 --- a/test/regress/regress0/bug484.smt2 +++ b/test/regress/regress0/bug484.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: -q ; EXPECT: sat ; Preamble -------------- diff --git a/test/regress/regress0/datatypes/issue2838.cvc b/test/regress/regress0/datatypes/issue2838.cvc index 95e1c898a..9fab5f423 100644 --- a/test/regress/regress0/datatypes/issue2838.cvc +++ b/test/regress/regress0/datatypes/issue2838.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: -q % EXPECT: sat Ints_0 : ARRAY INT OF INT; C : TYPE = [# i : INT #]; diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2 index e4e1f65b4..5d0d8f6e6 100644 --- a/test/regress/regress0/fmf/fmc_unsound_model.smt2 +++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat ; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc (set-logic ALL_SUPPORTED) diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 index d951e6c50..890e765aa 100644 --- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 +++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/arith/issue4985-model-success.smt2 b/test/regress/regress1/arith/issue4985-model-success.smt2 index 794eefb37..0249462ee 100644 --- a/test/regress/regress1/arith/issue4985-model-success.smt2 +++ b/test/regress/regress1/arith/issue4985-model-success.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_AUFNRA) (set-info :status sat) (declare-const arr0 (Array Real Real)) diff --git a/test/regress/regress1/arith/issue4985b-model-success.smt2 b/test/regress/regress1/arith/issue4985b-model-success.smt2 index eae8d369d..22b55c87f 100644 --- a/test/regress/regress1/arith/issue4985b-model-success.smt2 +++ b/test/regress/regress1/arith/issue4985b-model-success.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_AUFNRA) (set-info :status sat) (declare-const a (Array Real Real)) diff --git a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 index f1d20befc..33c1796f9 100644 --- a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 +++ b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2 index c4a40ccc1..4bf21d533 100644 --- a/test/regress/regress1/fmf/german169.smt2 +++ b/test/regress/regress1/fmf/german169.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/fmf/issue3626.smt2 b/test/regress/regress1/fmf/issue3626.smt2 index 25dc80223..6162b4cfe 100644 --- a/test/regress/regress1/fmf/issue3626.smt2 +++ b/test/regress/regress1/fmf/issue3626.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound --no-cegqi +; COMMAND-LINE: --fmf-bound --no-cegqi -q ; EXPECT: sat (set-logic ALL) (assert (forall ((a Int)) (or (distinct (/ 0 0) a) (= (/ 0 a) 0)))) diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 index 7f3a5b28f..8c72672cd 100644 --- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 +++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2 index 378380779..d32c1730e 100644 --- a/test/regress/regress1/fmf/loopy_coda.smt2 +++ b/test/regress/regress1/fmf/loopy_coda.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone +; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 index b2c42d7c5..3d30ae058 100644 --- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 +++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel +; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil)))) diff --git a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc index 5d1289997..7577e3966 100644 --- a/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc +++ b/test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: -q % EXPECT: sat OPTION "produce-models"; OPTION "fmf-bound"; diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2 index 25851f6e0..73de1a36f 100644 --- a/test/regress/regress1/fmf/nun-0208-to.smt2 +++ b/test/regress/regress1/fmf/nun-0208-to.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find +; COMMAND-LINE: --finite-model-find -q ; EXPECT: sat (set-logic ALL_SUPPORTED) (declare-sort b__ 0) diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 index 841d050a7..25662d6eb 100644 --- a/test/regress/regress1/ho/issue4065-no-rep.smt2 +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic AUFBV) (set-info :status sat) (set-option :bv-div-zero-const false) diff --git a/test/regress/regress1/quantifiers/issue5470-aext.smt2 b/test/regress/regress1/quantifiers/issue5470-aext.smt2 index 500ef6d4c..8846fe7fa 100644 --- a/test/regress/regress1/quantifiers/issue5470-aext.smt2 +++ b/test/regress/regress1/quantifiers/issue5470-aext.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic NIA) (set-option :strings-exp true) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 index 9e8cd6586..d45d72253 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 index e9883297e..c7ef2d053 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 index 2c42744ac..17028065c 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 index f24aa6b1b..95608c150 100644 --- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 index dbb653351..151499d78 100644 --- a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 +++ b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/sets/is_singleton1.smt2 b/test/regress/regress1/sets/is_singleton1.smt2 index 01b633d8e..f985961df 100644 --- a/test/regress/regress1/sets/is_singleton1.smt2 +++ b/test/regress/regress1/sets/is_singleton1.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) (declare-fun S () (Set Int)) @@ -6,4 +8,4 @@ (assert (= (singleton x) S)) (assert (is_singleton S)) (assert (is_singleton (singleton 3))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2 index ba8180b5e..75ac15817 100644 --- a/test/regress/regress1/sets/issue5271.smt2 +++ b/test/regress/regress1/sets/issue5271.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun s () (Set Int)) diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc b/test/regress/regress1/sets/sets-tuple-poly.cvc index 4cac9a24e..194129518 100644 --- a/test/regress/regress1/sets/sets-tuple-poly.cvc +++ b/test/regress/regress1/sets/sets-tuple-poly.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: -q % EXPECT: sat OPTION "sets-ext"; OPTION "logic" "ALL_SUPPORTED"; diff --git a/test/regress/regress1/sets/univ-set-uf-elim.smt2 b/test/regress/regress1/sets/univ-set-uf-elim.smt2 index a22f2a44f..f02788a72 100644 --- a/test/regress/regress1/sets/univ-set-uf-elim.smt2 +++ b/test/regress/regress1/sets/univ-set-uf-elim.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --produce-models ; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.") ; EXIT: 1 (set-logic ALL) diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 index 78035790b..fd2060942 100644 --- a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 +++ b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference +; COMMAND-LINE: --sygus-inference -q (set-logic ALL) (declare-fun a () Int) (declare-fun b () Int) diff --git a/test/regress/regress1/trim.cvc b/test/regress/regress1/trim.cvc index 8bdbde79a..019b7702f 100644 --- a/test/regress/regress1/trim.cvc +++ b/test/regress/regress1/trim.cvc @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find -q % EXPECT: sat DATATYPE myType = A | B diff --git a/test/regress/regress2/bv_to_int_5095_2.smt2 b/test/regress/regress2/bv_to_int_5095_2.smt2 index 54dfa0946..234e82229 100644 --- a/test/regress/regress2/bv_to_int_5095_2.smt2 +++ b/test/regress/regress2/bv_to_int_5095_2.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat -; COMMAND --solve-bv-as-int=sum +; COMMAND-LINE: --solve-bv-as-int=sum -q (set-logic BV) (declare-const bv_42-0 (_ BitVec 42)) (assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2 index 938aa01ea..b688d3fcf 100644 --- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 +++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic UFDTLIRA) (set-option :fmf-bound true) (set-option :finite-model-find true) |