From af874a5c7a2ff134da0d4c20d06a0626d3e36d9b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 May 2020 21:48:01 -0500 Subject: [PATCH] Do not eliminate variables that are equal to unevaluatable terms (#4267) When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled. This PR ensures we only eliminate variables when v contains only evaluated operators. Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change. Fixes #4500. --- src/expr/node_algorithm.cpp | 28 +++++++++++++ src/expr/node_algorithm.h | 8 ++++ src/theory/arith/theory_arith.cpp | 12 ++++++ src/theory/arith/theory_arith.h | 2 + src/theory/arith/theory_arith_private.cpp | 13 ++---- src/theory/arrays/theory_arrays.cpp | 6 +-- src/theory/builtin/theory_builtin.cpp | 11 +++-- src/theory/bv/theory_bv.cpp | 13 +++--- src/theory/quantifiers/theory_quantifiers.cpp | 2 + src/theory/sets/theory_sets.cpp | 38 +++++++++++++++++- src/theory/sets/theory_sets_private.cpp | 40 ------------------- src/theory/sets/theory_sets_private.h | 2 - src/theory/strings/theory_strings.cpp | 7 ++++ src/theory/strings/theory_strings.h | 3 ++ src/theory/theory.cpp | 28 +++++++++++-- src/theory/theory.h | 18 ++++++++- src/theory/theory_model.cpp | 26 ++++++------ src/theory/theory_model.h | 11 ++++- test/regress/CMakeLists.txt | 1 + .../quant-model-simplification.smt2 | 9 +++++ .../regress1/ho/nested_lambdas-AGT034^2.smt2 | 4 +- .../ho/nested_lambdas-sat-SYO056^1-delta.smt2 | 5 +-- test/regress/regress1/sets/choose1.smt2 | 2 +- test/regress/regress1/sets/choose4.smt2 | 6 +-- 24 files changed, 199 insertions(+), 96 deletions(-) create mode 100644 test/regress/regress0/quantifiers/quant-model-simplification.smt2 diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 0c572f615..44430f072 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -155,6 +155,34 @@ bool hasSubtermKind(Kind k, Node n) return false; } +bool hasSubtermKinds(const std::unordered_set& ks, + Node n) +{ + if (ks.empty()) + { + return false; + } + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + if (ks.find(cur.getKind()) != ks.end()) + { + return true; + } + visited.insert(cur); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } while (!visit.empty()); + return false; +} + bool hasSubterm(TNode n, const std::vector& t, bool strict) { if (t.empty()) diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 5e042d591..894dce7c6 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -51,6 +51,14 @@ bool hasSubtermMulti(TNode n, TNode t); */ bool hasSubtermKind(Kind k, Node n); +/** + * @param ks The kinds of node to check + * @param n The node to search in. + * @return true iff there is a term in n that has any kind ks + */ +bool hasSubtermKinds(const std::unordered_set& ks, + Node n); + /** * Check if the node n has a subterm that occurs in t. * @param n The node to search in diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index cdb6c77f3..e65369f96 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -63,6 +63,18 @@ void TheoryArith::preRegisterTerm(TNode n){ d_internal->preRegisterTerm(n); } +void TheoryArith::finishInit() +{ + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + if (getLogicInfo().isTheoryEnabled(THEORY_ARITH) + && getLogicInfo().areTranscendentalsUsed()) + { + // witness is used to eliminate square root + tm->setUnevaluatedKind(kind::WITNESS); + } +} + Node TheoryArith::expandDefinition(Node node) { return d_internal->expandDefinition(node); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index f15db32a1..8672f7145 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -58,6 +58,8 @@ public: */ void preRegisterTerm(TNode n) override; + void finishInit() override; + Node expandDefinition(Node node) override; void setMasterEqualityEngine(eq::EqualityEngine* eq) override; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0f2f4bbf4..7fdab2034 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1337,7 +1337,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o if (m.getVarList().singleton()){ VarList vl = m.getVarList(); Node var = vl.getNode(); - if (var.getKind() == kind::VARIABLE){ + if (var.isVar()) + { // if vl.isIntegral then m.getConstant().isOne() if(!vl.isIntegral() || m.getConstant().isOne()){ minVar = var; @@ -1362,15 +1363,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o << minVar << ":" << elim << endl; Debug("simplify") << right.size() << endl; } - else if (expr::hasSubterm(elim, minVar)) - { - Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute " - "due to recursive pattern with sharing: " - << minVar << ":" << elim << endl; - } - else if (!minVar.getType().isInteger() || right.isIntegral()) + else if (d_containing.isLegalElimination(minVar, elim)) { - Assert(!expr::hasSubterm(elim, minVar)); // cannot eliminate integers here unless we know the resulting // substitution is integral Debug("simplify") << "TheoryArithPrivate::solve(): substitution " @@ -1382,7 +1376,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o else { Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute " - "b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl; } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index e4b1e1c4c..5085c00ec 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -355,14 +355,12 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs { d_ppFacts.push_back(in); d_ppEqualityEngine.assertEquality(in, true, in); - if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]) - && (in[1].getType()).isSubtypeOf(in[0].getType())) + if (in[0].isVar() && isLegalElimination(in[0], in[1])) { outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]) - && (in[0].getType()).isSubtypeOf(in[1].getType())) + if (in[1].isVar() && isLegalElimination(in[1], in[0])) { outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1667e5505..a49903f13 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -43,10 +43,13 @@ std::string TheoryBuiltin::identify() const void TheoryBuiltin::finishInit() { - // choice nodes are not evaluated in getModelValue - TheoryModel* theoryModel = d_valuation.getModel(); - Assert(theoryModel != nullptr); - theoryModel->setUnevaluatedKind(kind::WITNESS); + // Notice that choice is an unevaluated kind belonging to this theory. + // However, it should be set as an unevaluated kind where it is used, e.g. + // in the quantifiers theory. This ensures that a logic like QF_LIA, which + // includes the builtin theory, does not mark any kinds as unevaluated and + // hence it is easy to check for illegal eliminations via TheoryModel + // (see TheoryModel::isLegalElimination) since there are no unevaluated kinds + // present. } } // namespace builtin diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 32791415e..fd8459641 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -634,13 +634,13 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, { case kind::EQUAL: { - if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])) + if (in[0].isVar() && isLegalElimination(in[0], in[1])) { ++(d_statistics.d_solveSubstitutions); outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])) + if (in[1].isVar() && isLegalElimination(in[1], in[0])) { ++(d_statistics.d_solveSubstitutions); outSubstitutions.addSubstitution(in[1], in[0]); @@ -652,7 +652,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, && node[0].isConst())) { Node extract = node[0].isConst() ? node[1] : node[0]; - if (extract[0].getKind() == kind::VARIABLE) + if (extract[0].isVar()) { Node c = node[0].isConst() ? node[0] : node[1]; @@ -688,8 +688,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, } Node concat = utils::mkConcat(children); Assert(utils::getSize(concat) == utils::getSize(extract[0])); - outSubstitutions.addSubstitution(extract[0], concat); - return PP_ASSERT_STATUS_SOLVED; + if (isLegalElimination(extract[0], concat)) + { + outSubstitutions.addSubstitution(extract[0], concat); + return PP_ASSERT_STATUS_SOLVED; + } } } } diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6407e0d6d..9242bec7c 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -58,6 +58,8 @@ void TheoryQuantifiers::finishInit() Assert(tm != nullptr); tm->setUnevaluatedKind(EXISTS); tm->setUnevaluatedKind(FORALL); + // witness is used in several instantiation strategies + tm->setUnevaluatedKind(WITNESS); } void TheoryQuantifiers::preRegisterTerm(TNode n) { diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 8430987f2..b5c2590d5 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -56,6 +56,8 @@ void TheorySets::finishInit() TheoryModel* tm = d_valuation.getModel(); Assert(tm != nullptr); tm->setUnevaluatedKind(COMPREHENSION); + // choice is used to eliminate witness + tm->setUnevaluatedKind(WITNESS); } void TheorySets::addSharedTerm(TNode n) { @@ -123,7 +125,41 @@ Node TheorySets::expandDefinition(Node n) } Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - return d_internal->ppAssert( in, outSubstitutions ); + Debug("sets-proc") << "ppAssert : " << in << std::endl; + Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED; + + // this is based off of Theory::ppAssert + if (in.getKind() == kind::EQUAL) + { + if (in[0].isVar() && isLegalElimination(in[0], in[1])) + { + // We cannot solve for sets if setsExt is enabled, since universe set + // may appear when this option is enabled, and solving for such a set + // impacts the semantics of universe set, see + // regress0/sets/pre-proc-univ.smt2 + if (!in[0].getType().isSet() || !options::setsExt()) + { + outSubstitutions.addSubstitution(in[0], in[1]); + status = Theory::PP_ASSERT_STATUS_SOLVED; + } + } + else if (in[1].isVar() && isLegalElimination(in[1], in[0])) + { + if (!in[0].getType().isSet() || !options::setsExt()) + { + outSubstitutions.addSubstitution(in[1], in[0]); + status = Theory::PP_ASSERT_STATUS_SOLVED; + } + } + else if (in[0].isConst() && in[1].isConst()) + { + if (in[0] != in[1]) + { + status = Theory::PP_ASSERT_STATUS_CONFLICT; + } + } + } + return status; } void TheorySets::presolve() { diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index fbf1e6fcf..78f6fa8b5 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1536,46 +1536,6 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType) return chooseSkolem; } -Theory::PPAssertStatus TheorySetsPrivate::ppAssert( - TNode in, SubstitutionMap& outSubstitutions) -{ - Debug("sets-proc") << "ppAssert : " << in << std::endl; - Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED; - - // TODO: allow variable elimination for sets when setsExt = true - - // this is based off of Theory::ppAssert - if (in.getKind() == kind::EQUAL) - { - if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]) - && (in[1].getType()).isSubtypeOf(in[0].getType())) - { - if (!in[0].getType().isSet() || !options::setsExt()) - { - outSubstitutions.addSubstitution(in[0], in[1]); - status = Theory::PP_ASSERT_STATUS_SOLVED; - } - } - else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]) - && (in[0].getType()).isSubtypeOf(in[1].getType())) - { - if (!in[1].getType().isSet() || !options::setsExt()) - { - outSubstitutions.addSubstitution(in[1], in[0]); - status = Theory::PP_ASSERT_STATUS_SOLVED; - } - } - else if (in[0].isConst() && in[1].isConst()) - { - if (in[0] != in[1]) - { - status = Theory::PP_ASSERT_STATUS_CONFLICT; - } - } - } - return status; -} - void TheorySetsPrivate::presolve() { d_state.reset(); } /**************************** eq::NotifyClass *****************************/ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index a7e6f69ee..da42ad1fe 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -210,8 +210,6 @@ class TheorySetsPrivate { * so that it makes theory-specific calls to evaluate interpreted symbols. */ Node expandDefinition(Node n); - - Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); void presolve(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b98bd1dea..6f3b4c0cb 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -135,6 +135,13 @@ TheoryStrings::~TheoryStrings() { } +void TheoryStrings::finishInit() +{ + TheoryModel* tm = d_valuation.getModel(); + // witness is used to eliminate str.from_code + tm->setUnevaluatedKind(WITNESS); +} + bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 2e78198e3..7c99b6968 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -108,6 +108,9 @@ class TheoryStrings : public Theory { const LogicInfo& logicInfo); ~TheoryStrings(); + /** finish initialization */ + void finishInit() override; + TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } void setMasterEqualityEngine(eq::EqualityEngine* eq) override; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 635a3216a..3069461fa 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -268,6 +268,28 @@ void Theory::debugPrintFacts() const{ printFacts(DebugChannel.getStream()); } +bool Theory::isLegalElimination(TNode x, TNode val) +{ + Assert(x.isVar()); + if (expr::hasSubterm(val, x)) + { + return false; + } + if (!val.getType().isSubtypeOf(x.getType())) + { + return false; + } + if (!options::produceModels()) + { + // don't care about the model, we are fine + return true; + } + // if there is a model object + TheoryModel* tm = d_valuation.getModel(); + Assert(tm != nullptr); + return tm->isLegalElimination(x, val); +} + std::unordered_set Theory::currentlySharedTerms() const{ std::unordered_set currentlyShared; for (shared_terms_iterator i = shared_terms_begin(), @@ -337,15 +359,13 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, // 1) x is a variable // 2) x is not in the term t // 3) x : T and t : S, then S <: T - if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]) - && (in[1].getType()).isSubtypeOf(in[0].getType()) + if (in[0].isVar() && isLegalElimination(in[0], in[1]) && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE) { outSubstitutions.addSubstitution(in[0], in[1]); return PP_ASSERT_STATUS_SOLVED; } - if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]) - && (in[0].getType()).isSubtypeOf(in[1].getType()) + if (in[1].isVar() && isLegalElimination(in[1], in[0]) && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE) { outSubstitutions.addSubstitution(in[1], in[0]); diff --git a/src/theory/theory.h b/src/theory/theory.h index c777f164f..366a943ef 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -248,8 +248,24 @@ class Theory { void printFacts(std::ostream& os) const; void debugPrintFacts() const; -public: + /** is legal elimination + * + * Returns true if x -> val is a legal elimination of variable x. This is + * useful for ppAssert, when x = val is an entailed equality. This function + * determines whether indeed x can be eliminated from the problem via the + * substituion x -> val. + * + * The following criteria imply that x -> val is *not* a legal elimination: + * (1) If x is contained in val, + * (2) If the type of val is not a subtype of the type of x, + * (3) If val contains an operator that cannot be evaluated, and produceModels + * is true. For example, x -> sqrt(2) is not a legal elimination if we + * are producing models. This is because we care about the value of x, and + * its value must be computed (approximated) by the non-linear solver. + */ + bool isLegalElimination(TNode x, TNode val); + public: /** * Return the ID of the theory responsible for the given type. */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index f24e4fc66..567b5c4e4 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -13,6 +13,7 @@ **/ #include "theory/theory_model.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/uf_options.h" @@ -56,7 +57,6 @@ TheoryModel::TheoryModel(context::Context* c, { setSemiEvaluatedKind(kind::APPLY_UF); } - setUnevaluatedKind(kind::BOUND_VARIABLE); } TheoryModel::~TheoryModel() @@ -203,19 +203,20 @@ Node TheoryModel::getModelValue(TNode n) const } Debug("model-getvalue-debug") << "Get model value " << n << " ... "; Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl; - if (n.isConst()) + Kind nk = n.getKind(); + if (n.isConst() || nk == BOUND_VARIABLE) { d_modelCache[n] = n; return n; } Node ret = n; - Kind nk = n.getKind(); NodeManager* nm = NodeManager::currentNM(); // if it is an evaluated kind, compute model values for children and evaluate if (n.getNumChildren() > 0 - && d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end()) + && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end() + && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end()) { Debug("model-getvalue-debug") << "Get model value children " << n << std::endl; @@ -308,10 +309,8 @@ Node TheoryModel::getModelValue(TNode n) const } // if we are a evaluated or semi-evaluated kind, return an arbitrary value - // if we are not in the d_not_evaluated_kinds map, we are evaluated - // if we are in the d_semi_evaluated_kinds, we are semi-evaluated - if (d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end() - || d_semi_evaluated_kinds.find(nk) != d_semi_evaluated_kinds.end()) + // if we are not in the d_unevaluated_kinds map, we are evaluated + if (d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()) { if (t.isFunction() || t.isPredicate()) { @@ -617,17 +616,18 @@ void TheoryModel::recordModelCoreSymbol(Expr sym) d_model_core.insert(Node::fromExpr(sym)); } -void TheoryModel::setUnevaluatedKind(Kind k) -{ - d_not_evaluated_kinds.insert(k); -} +void TheoryModel::setUnevaluatedKind(Kind k) { d_unevaluated_kinds.insert(k); } void TheoryModel::setSemiEvaluatedKind(Kind k) { - d_not_evaluated_kinds.insert(k); d_semi_evaluated_kinds.insert(k); } +bool TheoryModel::isLegalElimination(TNode x, TNode val) +{ + return !expr::hasSubtermKinds(d_unevaluated_kinds, val); +} + bool TheoryModel::hasTerm(TNode a) { return d_equalityEngine->hasTerm( a ); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index d984fbc6b..1deec82d9 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -266,6 +266,13 @@ public: */ void setUnevaluatedKind(Kind k); void setSemiEvaluatedKind(Kind k); + /** is legal elimination + * + * Returns true if x -> val is a legal elimination of variable x. + * In particular, this ensures that val does not have any subterms that + * are of unevaluated kinds. + */ + bool isLegalElimination(TNode x, TNode val); //---------------------------- end building the model // ------------------- general equality queries @@ -356,8 +363,8 @@ public: std::map d_approximations; /** list of all approximations */ std::vector > d_approx_list; - /** a set of kinds that are not evaluated */ - std::unordered_set d_not_evaluated_kinds; + /** a set of kinds that are unevaluated */ + std::unordered_set d_unevaluated_kinds; /** a set of kinds that are semi-evaluated */ std::unordered_set d_semi_evaluated_kinds; /** diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8a9151c17..6f948b02b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -766,6 +766,7 @@ set(regress_0_tests regress0/quantifiers/qbv-test-invert-concat-1.smt2 regress0/quantifiers/qbv-test-invert-sign-extend.smt2 regress0/quantifiers/qcf-rel-dom-opt.smt2 + regress0/quantifiers/quant-model-simplification.smt2 regress0/quantifiers/rew-to-scala.smt2 regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 diff --git a/test/regress/regress0/quantifiers/quant-model-simplification.smt2 b/test/regress/regress0/quantifiers/quant-model-simplification.smt2 new file mode 100644 index 000000000..ce75aff18 --- /dev/null +++ b/test/regress/regress0/quantifiers/quant-model-simplification.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(declare-sort U 0) +(declare-fun b () Int) +(declare-fun P (U) Bool) +(assert (= b (ite (forall ((x U)) (P x)) 2 3))) +(check-sat) diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 index 2818452b8..731fd4431 100644 --- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-check-proofs +; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-check-proofs --no-produce-models ; EXPECT: unsat (set-logic ALL) @@ -98,4 +98,4 @@ (assert (not (mvalid (very_much_likes jan cola)))) (set-info :filename "AGT034^2") -(check-sat) \ No newline at end of file +(check-sat) diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 index 9211adfb5..6743e00d4 100644 --- a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 @@ -28,10 +28,9 @@ (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Phi) Psi __flatten_var_0)))) -(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) -(assert (= mbox +(define-fun mbox () (-> (-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted Bool) (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) - (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) )))) + (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) ))) (assert (not (forall ((R (-> $$unsorted $$unsorted Bool))) (mvalid diff --git a/test/regress/regress1/sets/choose1.smt2 b/test/regress/regress1/sets/choose1.smt2 index 420a0fde0..0e937169e 100644 --- a/test/regress/regress1/sets/choose1.smt2 +++ b/test/regress/regress1/sets/choose1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-models +; COMMAND-LINE: --quiet (set-logic ALL) (set-info :status sat) (set-option :produce-models true) diff --git a/test/regress/regress1/sets/choose4.smt2 b/test/regress/regress1/sets/choose4.smt2 index df7c510d3..6cb97c3e3 100644 --- a/test/regress/regress1/sets/choose4.smt2 +++ b/test/regress/regress1/sets/choose4.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-models +; COMMAND-LINE: --quiet (set-logic ALL) (set-info :status sat) (set-option :produce-models true) @@ -6,8 +6,6 @@ (declare-fun a () Int) (assert (not (= A (as emptyset (Set Int))))) (assert (member 10 A)) -; this line raises an assertion error (assert (= a (choose A))) -; this line raises an assertion error ;(assert (exists ((x Int)) (and (= x (choose A)) (= x a)))) -(check-sat) \ No newline at end of file +(check-sat) -- 2.30.2