summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/booleans/circuit_propagator.h14
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.cpp13
-rw-r--r--src/theory/quantifiers/extended_rewrite.cpp151
-rw-r--r--src/theory/quantifiers/extended_rewrite.h12
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp45
-rw-r--r--src/theory/quantifiers/quant_conflict_find.h8
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_conjecture.cpp52
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_conjecture.h9
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_instantiation.cpp8
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.cpp88
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.h17
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp35
-rw-r--r--src/theory/theory_engine.cpp11
-rw-r--r--src/theory/theory_model_builder.cpp24
-rw-r--r--src/theory/theory_model_builder.h18
15 files changed, 372 insertions, 133 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index adb1eb42f..077a019fd 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -63,15 +63,13 @@ class CircuitPropagator
/**
* Construct a new CircuitPropagator.
*/
- CircuitPropagator(std::vector<Node>& outLearnedLiterals,
- bool enableForward = true,
- bool enableBackward = true)
+ CircuitPropagator(bool enableForward = true, bool enableBackward = true)
: d_context(),
d_propagationQueue(),
d_propagationQueueClearer(&d_context, d_propagationQueue),
d_conflict(&d_context, false),
- d_learnedLiterals(outLearnedLiterals),
- d_learnedLiteralClearer(&d_context, outLearnedLiterals),
+ d_learnedLiterals(),
+ d_learnedLiteralClearer(&d_context, d_learnedLiterals),
d_backEdges(),
d_backEdgesClearer(&d_context, d_backEdges),
d_seen(&d_context),
@@ -97,6 +95,8 @@ class CircuitPropagator
bool getNeedsFinish() { return d_needsFinish; }
+ std::vector<Node>& getLearnedLiterals() { return d_learnedLiterals; }
+
void finish() { d_context.pop(); }
/** Assert for propagation */
@@ -275,12 +275,12 @@ class CircuitPropagator
context::CDO<bool> d_conflict;
/** Map of substitutions */
- std::vector<Node>& d_learnedLiterals;
+ std::vector<Node> d_learnedLiterals;
/**
* Similar data clearer for learned literals.
*/
- DataClearer<std::vector<Node> > d_learnedLiteralClearer;
+ DataClearer<std::vector<Node>> d_learnedLiteralClearer;
/**
* Back edges from nodes to where they are used.
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index eb3f6232d..78fb987f1 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -426,6 +426,7 @@ int InstMatchGenerator::getNextMatch(Node f,
Node t = d_curr_first_candidate;
do{
Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
+ Assert(!qe->inConflict());
//if t not null, try to fit it into match m
if( !t.isNull() ){
if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
@@ -439,7 +440,7 @@ int InstMatchGenerator::getNextMatch(Node f,
}
//get the next candidate term t
if( success<0 ){
- t = d_cg->getNextCandidate();
+ t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
}else{
d_curr_first_candidate = d_cg->getNextCandidate();
}
@@ -1029,10 +1030,11 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
if( d_pol ){
tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
}else{
- Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
//iterate over all classes except r
tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
- if( tat ){
+ if (tat && !qe->inConflict())
+ {
+ Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
if( it->first!=r ){
InstMatch m( q );
@@ -1042,12 +1044,13 @@ int InstMatchGeneratorSimple::addInstantiations(Node q,
}
}
}
- tat = NULL;
}
+ tat = nullptr;
}
}
Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
- if( tat ){
+ if (tat && !qe->inConflict())
+ {
InstMatch m( q );
addInstantiations( m, qe, addedLemmas, 0, tat );
}
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 21a7fe29c..01454c3c7 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -20,6 +20,7 @@
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "theory/strings/theory_strings_rewriter.h"
using namespace CVC4::kind;
using namespace std;
@@ -207,6 +208,10 @@ Node ExtendedRewriter::extendedRewrite(Node n)
{
new_ret = extendedRewriteArith(ret);
}
+ else if (tid == THEORY_STRINGS)
+ {
+ new_ret = extendedRewriteStrings(ret);
+ }
}
//----------------------end theory-specific post-rewriting
@@ -1661,6 +1666,152 @@ Node ExtendedRewriter::extendedRewriteArith(Node ret)
return new_ret;
}
+Node ExtendedRewriter::extendedRewriteStrings(Node ret)
+{
+ Node new_ret;
+ Trace("q-ext-rewrite-debug")
+ << "Extended rewrite strings : " << ret << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ if (ret.getKind() == EQUAL)
+ {
+ if (ret[0].getType().isString())
+ {
+ Node tcontains[2];
+ bool tcontainsOneTrue = false;
+ unsigned tcontainsTrueIndex = 0;
+ for (unsigned i = 0; i < 2; i++)
+ {
+ Node tc = nm->mkNode(STRING_STRCTN, ret[i], ret[1 - i]);
+ tcontains[i] = Rewriter::rewrite(tc);
+ if (tcontains[i].isConst())
+ {
+ if (tcontains[i].getConst<bool>())
+ {
+ tcontainsOneTrue = true;
+ tcontainsTrueIndex = i;
+ }
+ else
+ {
+ new_ret = tcontains[i];
+ // if str.contains( x, y ) ---> false then x = y ---> false
+ // Notice we may not catch this in the rewriter for strings
+ // equality, since it only calls the specific rewriter for
+ // contains and not the full rewriter.
+ debugExtendedRewrite(ret, new_ret, "eq-contains-one-false");
+ return new_ret;
+ }
+ }
+ }
+ if (tcontainsOneTrue)
+ {
+ // if str.contains( x, y ) ---> true
+ // then x = y ---> contains( y, x )
+ new_ret = tcontains[1 - tcontainsTrueIndex];
+ debugExtendedRewrite(ret, new_ret, "eq-contains-one-true");
+ return new_ret;
+ }
+ else if (tcontains[0] == tcontains[1] && tcontains[0] != ret)
+ {
+ // if str.contains( x, y ) ---> t and str.contains( y, x ) ---> t,
+ // then x = y ---> t
+ new_ret = tcontains[0];
+ debugExtendedRewrite(ret, new_ret, "eq-dual-contains-eq");
+ return new_ret;
+ }
+
+ std::vector<Node> c[2];
+ for (unsigned i = 0; i < 2; i++)
+ {
+ strings::TheoryStringsRewriter::getConcat(ret[i], c[i]);
+ }
+
+ bool changed = false;
+ for (unsigned i = 0; i < 2; i++)
+ {
+ while (!c[0].empty() && !c[1].empty() && c[0].back() == c[1].back())
+ {
+ c[0].pop_back();
+ c[1].pop_back();
+ changed = true;
+ }
+ // splice constants
+ if (!c[0].empty() && !c[1].empty() && c[0].back().isConst()
+ && c[1].back().isConst())
+ {
+ String cs[2];
+ for (unsigned j = 0; j < 2; j++)
+ {
+ cs[j] = c[j].back().getConst<String>();
+ }
+ unsigned larger = cs[0].size() > cs[1].size() ? 0 : 1;
+ unsigned smallerSize = cs[1 - larger].size();
+ if (cs[1 - larger]
+ == (i == 0 ? cs[larger].suffix(smallerSize)
+ : cs[larger].prefix(smallerSize)))
+ {
+ unsigned sizeDiff = cs[larger].size() - smallerSize;
+ c[larger][c[larger].size() - 1] =
+ nm->mkConst(i == 0 ? cs[larger].prefix(sizeDiff)
+ : cs[larger].suffix(sizeDiff));
+ c[1 - larger].pop_back();
+ changed = true;
+ }
+ }
+ for (unsigned j = 0; j < 2; j++)
+ {
+ std::reverse(c[j].begin(), c[j].end());
+ }
+ }
+ if (changed)
+ {
+ // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y
+ Node s1 = strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, c[0]);
+ Node s2 = strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT, c[1]);
+ new_ret = s1.eqNode(s2);
+ debugExtendedRewrite(ret, new_ret, "string-eq-unify");
+ return new_ret;
+ }
+
+ // homogeneous constants
+ if (d_aggr)
+ {
+ for (unsigned i = 0; i < 2; i++)
+ {
+ if (ret[i].isConst())
+ {
+ bool isHomogeneous = true;
+ std::vector<unsigned> vec = ret[i].getConst<String>().getVec();
+ if (vec.size() > 1)
+ {
+ unsigned hchar = vec[0];
+ for (unsigned j = 1, size = vec.size(); j < size; j++)
+ {
+ if (vec[j] != hchar)
+ {
+ isHomogeneous = false;
+ break;
+ }
+ }
+ }
+ if (isHomogeneous && !std::is_sorted(c[1-i].begin(),c[1-i].end()))
+ {
+ Node ss = strings::TheoryStringsRewriter::mkConcat(STRING_CONCAT,
+ c[1 - i]);
+ Assert(ss != ret[1 - i]);
+ // e.g. "AA" = x ++ y ---> "AA" = y ++ x if y < x
+ new_ret = ret[i].eqNode(ss);
+ debugExtendedRewrite(ret, new_ret, "string-eq-homog-const");
+ return new_ret;
+ }
+ }
+ }
+ }
+ }
+ }
+
+ return new_ret;
+}
+
void ExtendedRewriter::debugExtendedRewrite(Node n,
Node ret,
const char* c) const
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 29f3b7bb3..da77bda51 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -231,8 +231,18 @@ class ExtendedRewriter
//--------------------------------------end generic utilities
//--------------------------------------theory-specific top-level calls
- /** extended rewrite arith */
+ /** extended rewrite arith
+ *
+ * If this method returns a non-null node ret', then ret is equivalent to
+ * ret'.
+ */
Node extendedRewriteArith(Node ret);
+ /** extended rewrite strings
+ *
+ * If this method returns a non-null node ret', then ret is equivalent to
+ * ret'.
+ */
+ Node extendedRewriteStrings(Node ret);
//--------------------------------------end theory-specific top-level calls
};
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 02c9aedf5..92a355348 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -268,7 +268,10 @@ bool QuantInfo::reset_round( QuantConflictFind * p ) {
d_mg->reset_round( p );
for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
- it->second->reset_round( p );
+ if (!it->second->reset_round(p))
+ {
+ return false;
+ }
}
//now, reset for matching
d_mg->reset( p, false, this );
@@ -1178,11 +1181,14 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars
}
}
-
-void MatchGen::reset_round( QuantConflictFind * p ) {
+bool MatchGen::reset_round(QuantConflictFind* p)
+{
d_wasSet = false;
for( unsigned i=0; i<d_children.size(); i++ ){
- d_children[i].reset_round( p );
+ if (!d_children[i].reset_round(p))
+ {
+ return false;
+ }
}
for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
@@ -1194,18 +1200,31 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
//}else if( e==-1 ){
// d_ground_eval[0] = p->d_false;
//}
- //modified
- for( unsigned i=0; i<2; i++ ){
- if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){
+ //modified
+ TermDb* tdb = p->getTermDatabase();
+ QuantifiersEngine* qe = p->getQuantifiersEngine();
+ for( unsigned i=0; i<2; i++ ){
+ if (tdb->isEntailed(d_n, i == 0))
+ {
d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
}
+ if (qe->inConflict())
+ {
+ return false;
+ }
}
}else if( d_type==typ_eq ){
- for (unsigned i = 0; i < d_n.getNumChildren(); i++)
+ TermDb* tdb = p->getTermDatabase();
+ QuantifiersEngine* qe = p->getQuantifiersEngine();
+ for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
{
if (!expr::hasBoundVar(d_n[i]))
{
- TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]);
+ TNode t = tdb->getEntailedTerm(d_n[i]);
+ if (qe->inConflict())
+ {
+ return false;
+ }
if (t.isNull())
{
d_ground_eval[i] = d_n[i];
@@ -1220,6 +1239,7 @@ void MatchGen::reset_round( QuantConflictFind * p ) {
d_qni_bound_cons.clear();
d_qni_bound_cons_var.clear();
d_qni_bound.clear();
+ return true;
}
void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
@@ -2038,9 +2058,10 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
}
}
Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
- if( d_conflict || d_quantEngine->inConflict() ){
- break;
- }
+ }
+ if (d_conflict || d_quantEngine->inConflict())
+ {
+ break;
}
}
}
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d76495b52..0469e958b 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -90,7 +90,13 @@ public:
std::vector< MatchGen > d_children;
short d_type;
bool d_type_not;
- void reset_round( QuantConflictFind * p );
+ /** reset round
+ *
+ * Called once at the beginning of each full/last-call effort, prior to
+ * processing this match generator. This method returns false if the reset
+ * failed, e.g. if a conflict was encountered during term indexing.
+ */
+ bool reset_round(QuantConflictFind* p);
void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
bool isValid() { return d_type!=typ_invalid; }
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index e3057da29..1d070417e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -70,6 +70,7 @@ void CegConjecture::assign( Node q ) {
Assert( q.getKind()==FORALL );
Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
d_quant = q;
+ NodeManager* nm = NodeManager::currentNM();
// pre-simplify the quantified formula based on the process utility
d_simp_quant = d_ceg_proc->preSimplify(d_quant);
@@ -163,10 +164,19 @@ void CegConjecture::assign( Node q ) {
}
// initialize the guard
- if (d_ceg_si->getGuard().isNull())
+ d_feasible_guard = nm->mkSkolem("G", nm->booleanType());
+ d_feasible_guard = Rewriter::rewrite(d_feasible_guard);
+ d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard);
+ AlwaysAssert(!d_feasible_guard.isNull());
+ // this must be called, both to ensure that the feasible guard is
+ // decided on with true polariy, but also to ensure that output channel
+ // has been used on this call to check.
+ d_qe->getOutputChannel().requirePhase(d_feasible_guard, true);
+
+ if (isSingleInvocation())
{
std::vector< Node > lems;
- d_ceg_si->getInitialSingleInvLemma( lems );
+ d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems);
for( unsigned i=0; i<lems.size(); i++ ){
Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation " << i << " : " << lems[i] << std::endl;
d_qe->getOutputChannel().lemma( lems[i] );
@@ -176,10 +186,9 @@ void CegConjecture::assign( Node q ) {
}
}
}
- Assert( !getGuard().isNull() );
- Node gneg = getGuard().negate();
+ Node gneg = d_feasible_guard.negate();
for( unsigned i=0; i<guarded_lemmas.size(); i++ ){
- Node lem = NodeManager::currentNM()->mkNode( OR, gneg, guarded_lemmas[i] );
+ Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]);
Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl;
d_qe->getOutputChannel().lemma( lem );
}
@@ -187,7 +196,7 @@ void CegConjecture::assign( Node q ) {
Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl;
}
-Node CegConjecture::getGuard() { return d_ceg_si->getGuard(); }
+Node CegConjecture::getGuard() const { return d_feasible_guard; }
bool CegConjecture::isSingleInvocation() const {
return d_ceg_si->isSingleInvocation();
@@ -196,20 +205,25 @@ bool CegConjecture::isSingleInvocation() const {
bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
return false;
- }else{
- bool value;
- Assert( !getGuard().isNull() );
- // non or fully single invocation : look at guard only
- if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) {
- if( !value ){
- Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
- return false;
- }
- }else{
- Assert( false );
+ }
+ bool value;
+ Assert(!d_feasible_guard.isNull());
+ // non or fully single invocation : look at guard only
+ if (d_qe->getValuation().hasSatValue(d_feasible_guard, value))
+ {
+ if (!value)
+ {
+ Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+ return false;
}
- return true;
}
+ else
+ {
+ Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard
+ << " is not assigned!" << std::endl;
+ Assert(false);
+ }
+ return true;
}
@@ -563,7 +577,7 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const
Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
// first, must try the guard
// which denotes "this conjecture is feasible"
- Node feasible_guard = getGuard();
+ Node feasible_guard = d_feasible_guard;
bool value;
if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
priority = 0;
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 25f063e06..48d307f1e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -97,8 +97,11 @@ public:
* module to get synthesis solutions.
*/
void getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation);
- /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */
- Node getGuard();
+ /**
+ * The feasible guard whose semantics are "this conjecture is feasiable".
+ * This is "G" in Figure 3 of Reynolds et al CAV 2015.
+ */
+ Node getGuard() const;
/** is ground */
bool isGround() { return d_inner_vars.empty(); }
/** are we using single invocation techniques */
@@ -132,6 +135,8 @@ public:
private:
/** reference to quantifier engine */
QuantifiersEngine * d_qe;
+ /** The feasible guard. */
+ Node d_feasible_guard;
/** single invocation utility */
std::unique_ptr<CegConjectureSingleInv> d_ceg_si;
/** utility for static preprocessing and analysis of conjectures */
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 1e0b36a3c..83a576d37 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -59,10 +59,10 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
d_waiting_conj = Node::null();
if (!d_conj->isAssigned())
{
- if (!assignConjecture(q))
- {
- return;
- }
+ assignConjecture(q);
+ // assign conjecture always uses the output channel, we return and
+ // re-check here.
+ return;
}
}
unsigned echeck =
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 39c3baf5c..7d8db8c03 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -49,12 +49,12 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe,
d_sip(new SingleInvocationPartition),
d_sol(new CegConjectureSingleInvSol(qe)),
d_cosi(new CegqiOutputSingleInv(this)),
- d_cinst(NULL),
+ d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)),
d_c_inst_match_trie(NULL),
- d_single_invocation(false) {
- // third and fourth arguments set to (false,false) until we have solution
- // reconstruction for delta and infinity
- d_cinst = new CegInstantiator(d_qe, d_cosi, false, false);
+ d_single_invocation(false)
+{
+ // The third and fourth arguments of d_cosi set to (false,false) until we have
+ // solution reconstruction for delta and infinity.
if (options::incrementalSolving()) {
d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext());
@@ -65,51 +65,53 @@ CegConjectureSingleInv::~CegConjectureSingleInv() {
if (d_c_inst_match_trie) {
delete d_c_inst_match_trie;
}
- delete d_cinst;
delete d_cosi;
delete d_sol; // (new CegConjectureSingleInvSol(qe)),
delete d_sip; // d_sip(new SingleInvocationPartition),
}
-void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) {
- Assert( d_si_guard.isNull() );
- //single invocation guard
- d_si_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
- d_si_guard = d_qe->getValuation().ensureLiteral( d_si_guard );
- AlwaysAssert( !d_si_guard.isNull() );
- d_qe->getOutputChannel().requirePhase( d_si_guard, true );
-
- if( !d_single_inv.isNull() ) {
- //make for new var/sk
- d_single_inv_var.clear();
- d_single_inv_sk.clear();
- Node inst;
- if( d_single_inv.getKind()==FORALL ){
- for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
- std::stringstream ss;
- ss << "k_" << d_single_inv[0][i];
- Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
- d_single_inv_var.push_back( d_single_inv[0][i] );
- d_single_inv_sk.push_back( k );
- d_single_inv_sk_index[k] = i;
- }
- inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
- }else{
- inst = d_single_inv;
- }
- inst = TermUtil::simpleNegate( inst );
- Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
-
- //register with the instantiator
- Node ginst = NodeManager::currentNM()->mkNode( OR, d_si_guard.negate(), inst );
- lems.push_back( ginst );
- //make and register the instantiator
- if( d_cinst ){
- delete d_cinst;
+void CegConjectureSingleInv::getInitialSingleInvLemma(Node g,
+ std::vector<Node>& lems)
+{
+ Assert(!g.isNull());
+ Assert(!d_single_inv.isNull());
+ // make for new var/sk
+ d_single_inv_var.clear();
+ d_single_inv_sk.clear();
+ Node inst;
+ NodeManager* nm = NodeManager::currentNM();
+ if (d_single_inv.getKind() == FORALL)
+ {
+ for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++)
+ {
+ std::stringstream ss;
+ ss << "k_" << d_single_inv[0][i];
+ Node k = nm->mkSkolem(ss.str(),
+ d_single_inv[0][i].getType(),
+ "single invocation function skolem");
+ d_single_inv_var.push_back(d_single_inv[0][i]);
+ d_single_inv_sk.push_back(k);
+ d_single_inv_sk_index[k] = i;
}
- d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
- d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
+ inst = d_single_inv[1].substitute(d_single_inv_var.begin(),
+ d_single_inv_var.end(),
+ d_single_inv_sk.begin(),
+ d_single_inv_sk.end());
}
+ else
+ {
+ inst = d_single_inv;
+ }
+ inst = TermUtil::simpleNegate(inst);
+ Trace("cegqi-si") << "Single invocation initial lemma : " << inst
+ << std::endl;
+
+ // register with the instantiator
+ Node ginst = nm->mkNode(OR, g.negate(), inst);
+ lems.push_back(ginst);
+ // make and register the instantiator
+ d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false));
+ d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk);
}
void CegConjectureSingleInv::initialize( Node q ) {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 00b50a4a1..09829e894 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -149,7 +149,7 @@ class CegConjectureSingleInv {
// the instantiator's output channel
CegqiOutputSingleInv* d_cosi;
// the instantiator
- CegInstantiator* d_cinst;
+ std::unique_ptr<CegInstantiator> d_cinst;
// list of skolems for each argument of programs
std::vector<Node> d_single_inv_arg_sk;
@@ -188,7 +188,6 @@ class CegConjectureSingleInv {
bool d_single_invocation;
// single invocation portion of quantified formula
Node d_single_inv;
- Node d_si_guard;
// transition relation version per program
std::map< Node, Node > d_trans_pre;
std::map< Node, Node > d_trans_post;
@@ -203,11 +202,17 @@ class CegConjectureSingleInv {
// get simplified conjecture
Node getSimplifiedConjecture() { return d_simp_quant; }
- // get single invocation guard
- Node getGuard() { return d_si_guard; }
public:
- //get the single invocation lemma(s)
- void getInitialSingleInvLemma( std::vector< Node >& lems );
+ /** get the single invocation lemma(s)
+ *
+ * This adds lemmas to lem that initializes this class for doing
+ * counterexample-guided instantiation for the synthesis conjecture. These
+ * lemmas correspond to the negation of the body of the (anti-skolemized)
+ * form of the conjecture for fresh skolems.
+ *
+ * Argument g is guard, for which all the above lemmas are guarded.
+ */
+ void getInitialSingleInvLemma(Node g, std::vector<Node>& lems);
// initialize this class for synthesis conjecture q
void initialize( Node q );
/** finish initialize
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 354115850..e09eefddc 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -911,6 +911,25 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
Node one = nm->mkConst(Rational(1));
retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
} else if( r.getKind() == kind::REGEXP_STAR ) {
+ if (x.isConst())
+ {
+ String s = x.getConst<String>();
+ if (s.size() == 0)
+ {
+ retNode = nm->mkConst(true);
+ // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
+ return returnRewrite(node, retNode, "re-empty-in-str-star");
+ }
+ else if (s.size() == 1)
+ {
+ if (r[0].getKind() == STRING_TO_REGEXP)
+ {
+ retNode = r[0][0].eqNode(x);
+ // e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x
+ return returnRewrite(node, retNode, "re-char-in-str-star");
+ }
+ }
+ }
if (r[0].getKind() == kind::REGEXP_SIGMA)
{
retNode = NodeManager::currentNM()->mkConst( true );
@@ -919,8 +938,6 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
bool allSigma = true;
bool allSigmaStrict = true;
unsigned allSigmaMinSize = 0;
- bool allString = true;
- std::vector< Node > cc;
for (const Node& rc : r)
{
Assert(rc.getKind() != kind::REGEXP_EMPTY);
@@ -935,14 +952,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
else
{
allSigma = false;
- }
- if (rc.getKind() != kind::STRING_TO_REGEXP)
- {
- allString = false;
- }
- else
- {
- cc.push_back(rc);
+ break;
}
}
if (allSigma)
@@ -952,11 +962,6 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
return returnRewrite(node, retNode, "re-concat-pure-allchar");
}
- else if (allString)
- {
- retNode = x.eqNode(mkConcat(STRING_CONCAT, cc));
- return returnRewrite(node, retNode, "re-concat-pure-str");
- }
}else if( r.getKind()==kind::REGEXP_INTER || r.getKind()==kind::REGEXP_UNION ){
std::vector< Node > mvec;
for( unsigned i=0; i<r.getNumChildren(); i++ ){
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d75f7843d..41ab45170 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -636,17 +636,12 @@ void TheoryEngine::check(Theory::Effort effort) {
AlwaysAssert(d_curr_model->isBuiltSuccess());
if (options::produceModels())
{
- // if we are incomplete, there is no guarantee on the model.
- // thus, we do not check the model here. (related to #1693)
- // we also don't debug-check the model if the checkModels()
- // is not enabled.
- if (!d_incomplete && options::checkModels())
- {
- d_curr_model_builder->debugCheckModel(d_curr_model);
- }
// Do post-processing of model from the theories (used for THEORY_SEP
// to construct heap model)
postProcessModel(d_curr_model);
+ // also call the model builder's post-process model
+ d_curr_model_builder->postProcessModel(d_incomplete.get(),
+ d_curr_model);
}
}
}
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index bcc4f7eaf..a9742b2ba 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -808,16 +808,30 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
{
return false;
}
- else
+
+ tm->d_modelBuiltSuccess = true;
+ return true;
+}
+
+void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
+{
+ // if we are incomplete, there is no guarantee on the model.
+ // thus, we do not check the model here. (related to #1693).
+ if (incomplete)
{
- tm->d_modelBuiltSuccess = true;
- return true;
+ return;
+ }
+ TheoryModel* tm = static_cast<TheoryModel*>(m);
+ Assert(tm != nullptr);
+ // debug-check the model if the checkModels() is enabled.
+ if (options::checkModels())
+ {
+ debugCheckModel(tm);
}
}
-void TheoryEngineModelBuilder::debugCheckModel(Model* m)
+void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
{
- TheoryModel* tm = (TheoryModel*)m;
#ifdef CVC4_ASSERTIONS
Assert(tm->isBuilt());
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 68e8c6b49..bff230b5c 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -68,13 +68,14 @@ class TheoryEngineModelBuilder : public ModelBuilder
* are building fails to satisfy a quantified formula.
*/
bool buildModel(Model* m) override;
- /** Debug check model.
+
+ /** postprocess model
*
- * This throws an assertion failure if the model
- * contains an equivalence class with two terms t1 and t2
- * such that t1^M != t2^M.
+ * This is called when m is a model that will be returned to the user. This
+ * method checks the internal consistency of the model if we are in a debug
+ * build.
*/
- void debugCheckModel(Model* m);
+ void postProcessModel(bool incomplete, Model* m);
protected:
/** pointer to theory engine */
@@ -102,6 +103,13 @@ class TheoryEngineModelBuilder : public ModelBuilder
virtual void debugModel(TheoryModel* m) {}
//-----------------------------------end virtual functions
+ /** Debug check model.
+ *
+ * This throws an assertion failure if the model contains an equivalence
+ * class with two terms t1 and t2 such that t1^M != t2^M.
+ */
+ void debugCheckModel(TheoryModel* m);
+
/** is n assignable?
*
* A term n is assignable if its value
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback