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.
return false;
}
+bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
+ Node n)
+{
+ if (ks.empty())
+ {
+ return false;
+ }
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::vector<TNode> 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<Node>& t, bool strict)
{
if (t.empty())
*/
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<Kind, kind::KindHashFunction>& ks,
+ Node n);
+
/**
* Check if the node n has a subterm that occurs in t.
* @param n The node to search in
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);
*/
void preRegisterTerm(TNode n) override;
+ void finishInit() override;
+
Node expandDefinition(Node node) override;
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
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;
<< 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 "
else
{
Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
- "b/c it's integer: "
<< minVar << ":" << minVar.getType() << " |-> "
<< elim << ":" << elim.getType() << endl;
}
{
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;
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
{
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]);
&& 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];
}
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;
+ }
}
}
}
Assert(tm != nullptr);
tm->setUnevaluatedKind(EXISTS);
tm->setUnevaluatedKind(FORALL);
+ // witness is used in several instantiation strategies
+ tm->setUnevaluatedKind(WITNESS);
}
void TheoryQuantifiers::preRegisterTerm(TNode n) {
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) {
}
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() {
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 *****************************/
* so that it makes theory-specific calls to evaluate interpreted symbols.
*/
Node expandDefinition(Node n);
-
- Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
void presolve();
}
+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));
const LogicInfo& logicInfo);
~TheoryStrings();
+ /** finish initialization */
+ void finishInit() override;
+
TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
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<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
for (shared_terms_iterator i = shared_terms_begin(),
// 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]);
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.
*/
**/
#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"
{
setSemiEvaluatedKind(kind::APPLY_UF);
}
- setUnevaluatedKind(kind::BOUND_VARIABLE);
}
TheoryModel::~TheoryModel()
}
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;
}
// 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())
{
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 );
*/
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
std::map<Node, Node> d_approximations;
/** list of all approximations */
std::vector<std::pair<Node, Node> > d_approx_list;
- /** a set of kinds that are not evaluated */
- std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds;
+ /** a set of kinds that are unevaluated */
+ std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
/** a set of kinds that are semi-evaluated */
std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
/**
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
--- /dev/null
+; 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)
-; 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)
(assert (not (mvalid (very_much_likes jan cola))))
(set-info :filename "AGT034^2")
-(check-sat)
\ No newline at end of file
+(check-sat)
(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
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE: --quiet
(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
-; COMMAND-LINE: --no-check-models
+; COMMAND-LINE: --quiet
(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(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)
projects / cvc5.git / commitdiff