Fixes #8094.
This makes it so that "value-like" terms can appear as subterms in other terms that are then subsequently also considered values. For example (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is now considered a value.
This also changes the default option for when to use witness terms for strings in models, based on some user feedback.
category = "regular"
long = "strings-model-max-len=N"
type = "uint64_t"
- default = "1000"
- maximum = "65536"
+ default = "65536"
help = "The maximum size of string values in models"
// Ensure it's a value (constant or const-ish like real algebraic
// numbers), or a lambda (for uninterpreted functions). This assertion only
// holds for models that do not have approximate values.
- if (!TheoryModel::isValue(resultNode))
+ if (!m->isValue(resultNode))
{
d_env->warning() << "Could not evaluate " << resultNode
<< " in getValue." << std::endl;
bool hasRelevantAssertions = false;
if (d_relManager != nullptr)
{
+ d_relManager->beginRound();
relevantAssertions =
d_relManager->getRelevantAssertions(hasRelevantAssertions);
+ d_relManager->endRound();
}
for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
if (val != d_true)
{
std::stringstream ss;
- ss << " " << theoryId
- << " has an asserted fact that the model doesn't satisfy." << endl
- << "The fact: " << assertion << endl
- << "Model value: " << val << endl;
+ ss << " " << theoryId << " has an asserted fact that";
+ if (val == d_false)
+ {
+ ss << " the model doesn't satisfy." << std::endl;
+ }
+ else
+ {
+ ss << " the model may not satisfy." << std::endl;
+ }
+ ss << "The fact: " << assertion << std::endl
+ << "Model value: " << val << std::endl;
if (hardFailure)
{
if (val == d_false)
*/
#include "theory/theory_model.h"
+#include "expr/attribute.h"
#include "expr/cardinality_constraint.h"
#include "expr/node_algorithm.h"
#include "options/quantifiers_options.h"
return ss.str();
}
-bool TheoryModel::isValue(TNode node)
+struct IsModelValueTag
{
- if (node.isConst())
+};
+struct IsModelValueComputedTag
+{
+};
+/** Attribute true for expressions that are quasi-values */
+using IsModelValueAttr = expr::Attribute<IsModelValueTag, bool>;
+using IsModelValueComputedAttr = expr::Attribute<IsModelValueComputedTag, bool>;
+
+bool TheoryModel::isBaseModelValue(TNode n) const
+{
+ if (n.isConst())
{
return true;
}
- Kind k = node.getKind();
- return k == kind::REAL_ALGEBRAIC_NUMBER || k == kind::LAMBDA
- || k == kind::WITNESS;
+ Kind k = n.getKind();
+ if (k == kind::REAL_ALGEBRAIC_NUMBER || k == kind::LAMBDA
+ || k == kind::WITNESS)
+ {
+ // we are a value if we are one of the above kinds
+ return true;
+ }
+ return false;
+}
+
+bool TheoryModel::isValue(TNode n) const
+{
+ IsModelValueAttr imva;
+ IsModelValueComputedAttr imvca;
+ // The list of nodes we are processing, and the current child index of that
+ // node we are inspecting. This vector always specifies a single path in the
+ // original term n. Notice this index accounts for operators, where the
+ // operator of a term is treated as the first child, and subsequently all
+ // other children are shifted up by one.
+ std::vector<std::pair<TNode, size_t>> visit;
+ // the last computed value of whether a node was a value
+ bool currentReturn = false;
+ visit.emplace_back(n, 0);
+ std::pair<TNode, size_t> v;
+ while (!visit.empty())
+ {
+ v = visit.back();
+ TNode cur = v.first;
+ bool finishedComputing = false;
+ // if we just pushed to the stack, do initial checks
+ if (v.second == 0)
+ {
+ if (cur.getAttribute(imvca))
+ {
+ // already cached
+ visit.pop_back();
+ currentReturn = cur.getAttribute(imva);
+ continue;
+ }
+ if (isBaseModelValue(cur))
+ {
+ finishedComputing = true;
+ currentReturn = true;
+ }
+ else if (cur.getNumChildren() == 0 || rewrite(cur) != cur)
+ {
+ finishedComputing = true;
+ currentReturn = false;
+ }
+ }
+ else if (!currentReturn)
+ {
+ // if the last child was not a value, we are not a value
+ finishedComputing = true;
+ }
+ if (!finishedComputing)
+ {
+ bool hasOperator = cur.hasOperator();
+ size_t nextChildIndex = v.second;
+ if (hasOperator && nextChildIndex > 0)
+ {
+ // if have an operator, we shift the child index we are looking at
+ nextChildIndex--;
+ }
+ if (nextChildIndex == cur.getNumChildren())
+ {
+ // finished, we are a value
+ currentReturn = true;
+ }
+ else
+ {
+ visit.back().second++;
+ if (hasOperator && v.second == 0)
+ {
+ // if we have an operator, process it as the first child
+ visit.emplace_back(cur.getOperator(), 0);
+ }
+ else
+ {
+ Assert(nextChildIndex < cur.getNumChildren());
+ // process the next child, which may be shifted from v.second to
+ // account for the operator
+ visit.emplace_back(cur[nextChildIndex], 0);
+ }
+ continue;
+ }
+ }
+ visit.pop_back();
+ cur.setAttribute(imva, currentReturn);
+ cur.setAttribute(imvca, true);
+ }
+ Assert(n.getAttribute(imvca));
+ return currentReturn;
}
} // namespace theory
std::string debugPrintModelEqc() const;
/**
- * Is the node n a "value"? This is true if n is constant, a constant-like
- * value (e.g. a real algebraic number) or if n is a lambda.
+ * Is the node n a "value"? This is true if n is a "base value", where
+ * a base value is one where isConst() returns true, a constant-like
+ * value (e.g. a real algebraic number) or if n is a lambda or witness
+ * term.
+ *
+ * We also return true for rewritten nodes whose leafs are base values.
+ * For example, (str.++ (witness ((x String)) (= (str.len x) 1000)) "A") is
+ * a value.
*/
- static bool isValue(TNode node);
+ bool isValue(TNode node) const;
protected:
/** Unique name of this model */
* a model builder constructs this model.
*/
virtual void addTermInternal(TNode n);
+ /**
+ * Is base model value? This is a helper method for isValue, returns true
+ * if n is a base model value.
+ */
+ bool isBaseModelValue(TNode n) const;
+
private:
/** cache for getModelValue */
mutable std::unordered_map<Node, Node> d_modelCache;
{
Trace("model-builder-debug") << "...try to normalize" << std::endl;
Node normalized = normalize(m, n, true);
- if (TheoryModel::isValue(normalized))
+ if (m->isValue(normalized))
{
return normalized;
}
// Members of exclusion set must have values, otherwise we are not yet
// assignable.
Node er = eset[i];
- if (TheoryModel::isValue(er))
+ if (tm->isValue(er))
{
// already processed
continue;
// applicable. We check if n is a value here, e.g. a term for which
// isConst returns true, or a lambda. The latter is required only for
// higher-order.
- if (TheoryModel::isValue(n))
+ if (tm->isValue(n))
{
Assert(constRep.isNull());
constRep = n;
}
if (!normalized.isNull())
{
- Assert(TheoryModel::isValue(normalized));
+ Assert(tm->isValue(normalized));
typeConstSet.add(tb, normalized);
assignConstantRep(tm, *i2, normalized);
Trace("model-builder") << " Eval: Setting constant rep of "
Trace("model-builder") << " Normalizing rep (" << rep
<< "), normalized to (" << normalized << ")"
<< endl;
- if (TheoryModel::isValue(normalized))
+ if (tm->isValue(normalized))
{
changed = true;
typeConstSet.add(tb, normalized);
{
ri = normalize(m, ri, evalOnly);
}
- if (!TheoryModel::isValue(ri))
+ if (!m->isValue(ri))
{
childrenConst = false;
}
regress1/nl/sugar-ident-3.smt2
regress1/nl/sugar-ident.smt2
regress1/nl/tan-rewrite2.smt2
+ regress1/nl/transcedental_model_simple.smt2
regress1/nl/zero-subset.smt2
regress1/non-fatal-errors.smt2
regress1/proj-issue175.smt2
regress1/strings/issue6973-dup-lemma-conc.smt2
regress1/strings/issue7677-test-const-rv.smt2
regress1/strings/issue7918-learned-rewrite.smt2
+ regress1/strings/issue8094-witness-model.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
regress1/strings/update-ex1.smt2
regress1/strings/update-ex2.smt2
regress1/strings/username_checker_min.smt2
+ regress1/strings/witness-model.smt2
regress1/sygus/VC22_a.sy
regress1/sygus/abv.sy
regress1/sygus/array-grammar-store.sy
; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_UFNRAT)
-(set-option :produce-models true)
+(set-info :status sat)
(declare-fun b (Real) Real)
(declare-fun v () Real)
(assert (distinct 0 (* v v)))
; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_NRAT)
+(set-info :status sat)
(set-option :re-elim-agg true)
(declare-fun r6 () Real)
(assert (= 0.0 (cos r6)))
--- /dev/null
+; COMMAND-LINE: --nl-rlv=always -q
+; EXPECT: sat
+(set-logic QF_NRAT)
+(set-info :status sat)
+(declare-fun x () Real)
+(assert (or (= x (sin 0.1)) (= x (sin 1.1))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun v () String)
+(declare-fun r () Bool)
+(declare-fun w () String)
+(declare-fun q () String)
+(assert (forall ((V String)) (or r (exists ((V String)) (str.in_re (str.++ "z" v) (re.* (str.to_re (str.from_code (str.len v)))))))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --strings-exp -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun w () String)
+(declare-fun q () String)
+(assert (= (str.len q) 99999999999999999999999999999999999999))
+(assert (= w (str.++ q "A")))
+(check-sat)
projects / cvc5.git / commitdiff