diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 151 | ||||
-rw-r--r-- | src/theory/quantifiers/extended_rewrite.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 45 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 52 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 88 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.h | 17 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 35 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 11 | ||||
-rw-r--r-- | src/theory/theory_model_builder.cpp | 24 | ||||
-rw-r--r-- | src/theory/theory_model_builder.h | 18 |
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 |