summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/datatypes_rewriter.cpp13
-rw-r--r--src/theory/quantifiers/candidate_rewrite_database.cpp6
-rw-r--r--src/theory/quantifiers/expr_miner.cpp9
-rw-r--r--src/theory/quantifiers/sygus/cegis.cpp1
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.h5
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp18
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.h8
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.cpp17
-rw-r--r--src/theory/strings/regexp_elim.cpp22
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp35
10 files changed, 102 insertions, 32 deletions
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index fe6764297..4469f0fe9 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -244,14 +244,21 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
return ret;
}
- Kind ok = getOperatorKindForSygusBuiltin(op);
- if (schildren.size() == 1 && ok == kind::UNDEFINED_KIND)
+ Kind ok = NodeManager::operatorToKind(op);
+ if (ok != UNDEFINED_KIND)
+ {
+ ret = NodeManager::currentNM()->mkNode(ok, schildren);
+ Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
+ return ret;
+ }
+ Kind tok = getOperatorKindForSygusBuiltin(op);
+ if (schildren.size() == 1 && tok == kind::UNDEFINED_KIND)
{
ret = schildren[0];
}
else
{
- ret = NodeManager::currentNM()->mkNode(ok, schildren);
+ ret = NodeManager::currentNM()->mkNode(tok, schildren);
}
Trace("dt-sygus-util") << "...return " << ret << std::endl;
return ret;
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 908bef92c..2d2e9ce30 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -276,11 +276,7 @@ CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen(
bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out)
{
- ExtendedRewriter* er = nullptr;
- if (options::synthRrPrepExtRew())
- {
- er = &d_ext_rewrite;
- }
+ ExtendedRewriter* er = &d_ext_rewrite;
Node nr;
if (er == nullptr)
{
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 0e8542826..67aa8688c 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -77,7 +77,8 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
// check is ground.
Node squery = convertToSkolem(query);
NodeManager* nm = NodeManager::currentNM();
- if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+ if (options::sygusExprMinerCheckTimeout.wasSetByUser()
+ || options::sygusRewSynthInput())
{
// To support a separate timeout for the subsolver, we need to create
// a separate ExprManager with its own options. This requires that
@@ -89,6 +90,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
checker.reset(new SmtEngine(&em));
checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
+ checker->setOption("sygus-rr-synth-input", false);
Expr equery = squery.toExpr().exportTo(&em, varMap);
checker->assertFormula(equery);
}
@@ -96,8 +98,9 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
{
std::stringstream msg;
msg << "Unable to export " << squery
- << " but exporting expressions is required for "
- "--sygus-rr-synth-check-timeout.";
+ << " but exporting expressions is "
+ "required for an expression "
+ "miner check.";
throw OptionException(msg.str());
}
needExport = true;
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 2e7f0cc02..06f041d93 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -198,6 +198,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
Node lem = nm->mkNode(
OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
lems.push_back(lem);
+ addedEvalLemmas = true;
Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
<< std::endl;
}
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index f9c10e33e..972d07af7 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -95,8 +95,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
* registerEvalPtAtSize on the output channel of d_qe.
*/
void registerEvalPts(const std::vector<Node>& eis, Node e);
- /** Retrieves active guard for enumerator */
- Node getActiveGuardForEnumerator(Node e);
private:
/** reference to quantifier engine */
@@ -109,9 +107,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
bool d_initialized;
/** null node */
Node d_null;
- /** map from condition enumerators to active guards (in case they are
- * enumerated indepedently of the return values) */
- std::map<Node, Node> d_enum_to_active_guard;
/** information per initialized type */
class StrategyPtInfo
{
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index eadbf766a..47c701cf6 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -126,21 +126,18 @@ Node CegGrammarConstructor::process(Node q,
preGrammarType = preGrammarType.getRangeType();
}
}
- Node sfvl = getSygusVarList(sf);
- // sfvl may be null for constant synthesis functions
- Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
// the actual sygus datatype we will use (normalized below)
TypeNode tn;
std::stringstream ss;
ss << sf;
- if (preGrammarType.isDatatype()
- && static_cast<DatatypeType>(preGrammarType.toType())
- .getDatatype()
- .isSygus())
+ Node sfvl;
+ if (preGrammarType.isDatatype() && preGrammarType.getDatatype().isSygus())
{
+ sfvl = Node::fromExpr(preGrammarType.getDatatype().getSygusVarList());
tn = preGrammarType;
}else{
+ sfvl = getSygusVarList(sf);
// check which arguments are irrelevant
std::unordered_set<unsigned> arg_irrelevant;
d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
@@ -156,6 +153,9 @@ Node CegGrammarConstructor::process(Node q,
tn = mkSygusDefaultType(
preGrammarType, sfvl, ss.str(), extra_cons, exc_cons, term_irlv);
}
+ // sfvl may be null for constant synthesis functions
+ Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is "
+ << sfvl << std::endl;
// normalize type
SygusGrammarNorm sygus_norm(d_qe);
@@ -367,6 +367,10 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
ops.push_back(nm->mkConst(true));
ops.push_back(nm->mkConst(false));
}
+ else if (type.isString())
+ {
+ ops.push_back(nm->mkConst(String("")));
+ }
// TODO #1178 : add other missing types
}
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 022031bef..0c5b67656 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -108,6 +108,12 @@ public:
* functions-to-synthesize of sygus conjecture q.
*/
static bool hasSyntaxRestrictions(Node q);
+ /**
+ * Make the builtin constants for type "type" that should be included in a
+ * sygus grammar, add them to vector ops.
+ */
+ static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
+
private:
/** reference to quantifier engine */
QuantifiersEngine * d_qe;
@@ -124,8 +130,6 @@ public:
//---------------- grammar construction
// helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
- // make the builtin constants for type type that should be included in a sygus grammar
- static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
// collect the list of types that depend on type range
static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
/** helper function for function mkSygusDefaultType
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index b014a30c6..b5dea4c38 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -158,12 +158,21 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
Node sygus_op = Node::fromExpr(cons.getSygusOp());
Trace("sygus-grammar-normalize-debug")
<< ".....operator is " << sygus_op << std::endl;
- Node exp_sop_n = Node::fromExpr(
- smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
+ Node exp_sop_n = sygus_op;
+ // Only expand definitions if the operator is not constant, since calling
+ // expandDefinitions on them should be a no-op. This check ensures we don't
+ // try to expand e.g. bitvector extract operators, whose type is undefined,
+ // and thus should not be passed to expandDefinitions.
+ if (!sygus_op.isConst())
+ {
+ exp_sop_n = Node::fromExpr(
+ smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
+ }
+ // get the kind for the operator.
+ Kind ok = NodeManager::operatorToKind(exp_sop_n);
// if it is a builtin operator, convert to total version if necessary
- if (exp_sop_n.getKind() == kind::BUILTIN)
+ if (ok != UNDEFINED_KIND)
{
- Kind ok = NodeManager::operatorToKind(sygus_op);
Kind nk = getEliminateKind(ok);
if (nk != ok)
{
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 8ea26fca9..0310e4620 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -104,18 +104,21 @@ Node RegExpElimination::eliminateConcat(Node atom)
// prev_end stores the current (symbolic) index in x that we are
// searching.
Node prev_end = d_zero;
+ // the symbolic index we start searching, for each child in sep_children.
+ std::vector<Node> prev_ends;
unsigned gap_minsize_end = gap_minsize.back();
bool gap_exact_end = gap_exact.back();
std::vector<Node> non_greedy_find_vars;
for (unsigned i = 0, size = sep_children.size(); i < size; i++)
{
- Node sc = sep_children[i];
if (gap_minsize[i] > 0)
{
// the gap to this child is at least gap_minsize[i]
prev_end =
nm->mkNode(PLUS, prev_end, nm->mkConst(Rational(gap_minsize[i])));
}
+ prev_ends.push_back(prev_end);
+ Node sc = sep_children[i];
Node lensc = nm->mkNode(STRING_LENGTH, sc);
if (gap_exact[i])
{
@@ -169,7 +172,6 @@ Node RegExpElimination::eliminateConcat(Node atom)
Node lenSc = nm->mkNode(STRING_LENGTH, sc);
Node loc = nm->mkNode(MINUS, lenx, nm->mkNode(PLUS, lenSc, cEnd));
Node scc = sc.eqNode(nm->mkNode(STRING_SUBSTR, x, loc, lenSc));
- conj.push_back(scc);
// We also must ensure that we fit. This constraint is necessary in
// addition to the constraint above. Take this example:
// x in (re.++ "A" _ (re.* _) "B" _) --->
@@ -182,9 +184,23 @@ Node RegExpElimination::eliminateConcat(Node atom)
// would have been the case than "ABB" would be a model for x, where
// the second constraint refers to the third position, and the third
// constraint refers to the second position.
+ //
+ // With respect to the above example, the following is an optimization.
+ // For that example, we instead produce:
+ // x in (re.++ "A" _ (re.* _) "B" _) --->
+ // substr( x, 0, 1 ) = "A" ^ // find "A"
+ // substr( x, len(x)-2, 1 ) = "B" ^ // "B" is at end - 2
+ // 2 <= len( x ) - 2
+ // The intuition is that above, there are two constraints that insist
+ // that "B" is found, whereas we only need one. The last constraint
+ // above says that the "B" we find at end-2 can be found >=1 after
+ // the "A".
+ conj.pop_back();
Node fit = nm->mkNode(gap_exact[sep_children.size() - 1] ? EQUAL : LEQ,
- nm->mkNode(MINUS, prev_end, lenSc),
+ prev_ends.back(),
loc);
+
+ conj.push_back(scc);
conj.push_back(fit);
}
else if (gap_minsize_end > 0)
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index b2778298a..00a711a31 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1610,6 +1610,33 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
return returnRewrite(node, ret, "ss-len-non-pos");
}
+ if (node[0].getKind() == STRING_SUBSTR)
+ {
+ // (str.substr (str.substr x a b) c d) ---> "" if c >= b
+ //
+ // Note that this rewrite can be generalized to:
+ //
+ // (str.substr x a b) ---> "" if a >= (str.len x)
+ //
+ // This can be done when we generalize our entailment methods to
+ // accept an optional context. Then we could conjecture that
+ // (str.substr x a b) rewrites to "" and do a case analysis:
+ //
+ // - a < 0 or b < 0 (the result is trivially empty in these cases)
+ // - a >= (str.len x) assuming that { a >= 0, b >= 0 }
+ //
+ // For example, for (str.substr (str.substr x a a) a a), we could
+ // then deduce that under those assumptions, "a" is an
+ // over-approximation of the length of (str.substr x a a), which
+ // then allows us to reason that the result of the whole term must
+ // be empty.
+ if (checkEntailArith(node[1], node[0][2]))
+ {
+ Node ret = nm->mkConst(::CVC4::String(""));
+ return returnRewrite(node, ret, "ss-start-geq-len");
+ }
+ }
+
std::vector<Node> n1;
getConcat(node[0], n1);
@@ -1673,6 +1700,14 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
Node ret = nm->mkConst(::CVC4::String(""));
return returnRewrite(node, ret, "ss-start-entails-zero-len");
}
+
+ // (str.substr s x x) ---> "" if (str.len s) <= 1
+ Node one = nm->mkConst(CVC4::Rational(1));
+ if (node[1] == node[2] && checkEntailArith(one, tot_len))
+ {
+ Node ret = nm->mkConst(::CVC4::String(""));
+ return returnRewrite(node, ret, "ss-len-one-z-z");
+ }
}
if (!curr.isNull())
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback