diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-11 16:25:28 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-11 16:25:28 -0700 |
commit | 589a6855997c37c46bc58c3eea30bf73b1a3c222 (patch) | |
tree | 0b9d8e4949a44a7ceebc15d4c2d8d7c336c31dd1 | |
parent | a6f694c852b22789a1cca9116ba5de4b6663ccce (diff) | |
parent | 6c6957ccee127548824062d282cc81270e5deb17 (diff) |
Merge branch 'master' into fixBetterSkolemsfixBetterSkolems
19 files changed, 612 insertions, 261 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9ba7f4b2e..b224032e8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1004,7 +1004,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; - sgt.d_expr = PARSER_STATE->getVariable(name); + sgt.d_expr = PARSER_STATE->getExpressionForName(name); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else{ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 303295112..2b81b3835 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4201,7 +4201,10 @@ Expr SmtEngine::getValue(const Expr& ex) const Trace("smt") << "--- model-post expected " << expectedType << endl; // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType), + // Notice that lambdas have function type, which does not respect the subtype + // relation, so we ignore them here. + Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA + || resultNode.getType().isSubtypeOf(expectedType), "Run with -t smt for details."); // ensure it's a constant diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 29b1cf2fc..1f6e1388a 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -3282,6 +3282,7 @@ std::vector<Node> NonlinearExtension::checkMonomialMagnitude( unsigned c ) { std::vector<Node> NonlinearExtension::checkTangentPlanes() { std::vector< Node > lemmas; Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); unsigned kstart = d_ms_vars.size(); for (unsigned k = kstart; k < d_mterms.size(); k++) { Node t = d_mterms[k]; @@ -3321,7 +3322,8 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { Node pt_v = d_tangent_val_bound[p][a][b]; Assert( !pt_v.isNull() ); if( curr_v!=pt_v ){ - Node do_extend = NodeManager::currentNM()->mkNode( ( p==1 || p==3 ) ? GT : LT, curr_v, pt_v ); + Node do_extend = + nm->mkNode((p == 1 || p == 3) ? GT : LT, curr_v, pt_v); do_extend = Rewriter::rewrite( do_extend ); if( do_extend==d_true ){ for( unsigned q=0; q<2; q++ ){ @@ -3340,26 +3342,69 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { Node b_v = pts[1][p]; // tangent plane - Node tplane = NodeManager::currentNM()->mkNode( - MINUS, - NodeManager::currentNM()->mkNode( - PLUS, - NodeManager::currentNM()->mkNode(MULT, b_v, a), - NodeManager::currentNM()->mkNode(MULT, a_v, b)), - NodeManager::currentNM()->mkNode(MULT, a_v, b_v)); + Node tplane = nm->mkNode(MINUS, + nm->mkNode(PLUS, + nm->mkNode(MULT, b_v, a), + nm->mkNode(MULT, a_v, b)), + nm->mkNode(MULT, a_v, b_v)); for (unsigned d = 0; d < 4; d++) { - Node aa = NodeManager::currentNM()->mkNode( - d == 0 || d == 3 ? GEQ : LEQ, a, a_v); - Node ab = NodeManager::currentNM()->mkNode( - d == 1 || d == 3 ? GEQ : LEQ, b, b_v); - Node conc = NodeManager::currentNM()->mkNode( - d <= 1 ? LEQ : GEQ, t, tplane); - Node tlem = NodeManager::currentNM()->mkNode( - OR, aa.negate(), ab.negate(), conc); + Node aa = nm->mkNode(d == 0 || d == 3 ? GEQ : LEQ, a, a_v); + Node ab = nm->mkNode(d == 1 || d == 3 ? GEQ : LEQ, b, b_v); + Node conc = nm->mkNode(d <= 1 ? LEQ : GEQ, t, tplane); + Node tlem = nm->mkNode(OR, aa.negate(), ab.negate(), conc); Trace("nl-ext-tplanes") << "Tangent plane lemma : " << tlem << std::endl; lemmas.push_back(tlem); } + + // tangent plane reverse implication + + // t <= tplane -> ( (a <= a_v ^ b >= b_v) v + // (a >= a_v ^ b <= b_v) ). + // in clause form, the above becomes + // t <= tplane -> a <= a_v v b <= b_v. + // t <= tplane -> b >= b_v v a >= a_v. + Node a_leq_av = nm->mkNode(LEQ, a, a_v); + Node b_leq_bv = nm->mkNode(LEQ, b, b_v); + Node a_geq_av = nm->mkNode(GEQ, a, a_v); + Node b_geq_bv = nm->mkNode(GEQ, b, b_v); + + Node t_leq_tplane = nm->mkNode(LEQ, t, tplane); + Node a_leq_av_or_b_leq_bv = nm->mkNode(OR, a_leq_av, b_leq_bv); + Node b_geq_bv_or_a_geq_av = nm->mkNode(OR, b_geq_bv, a_geq_av); + Node ub_reverse1 = + nm->mkNode(OR, t_leq_tplane.negate(), a_leq_av_or_b_leq_bv); + Trace("nl-ext-tplanes") + << "Tangent plane lemma (reverse) : " << ub_reverse1 + << std::endl; + lemmas.push_back(ub_reverse1); + Node ub_reverse2 = + nm->mkNode(OR, t_leq_tplane.negate(), b_geq_bv_or_a_geq_av); + Trace("nl-ext-tplanes") + << "Tangent plane lemma (reverse) : " << ub_reverse2 + << std::endl; + lemmas.push_back(ub_reverse2); + + // t >= tplane -> ( (a <= a_v ^ b <= b_v) v + // (a >= a_v ^ b >= b_v) ). + // in clause form, the above becomes + // t >= tplane -> a <= a_v v b >= b_v. + // t >= tplane -> b >= b_v v a <= a_v + Node t_geq_tplane = nm->mkNode(GEQ, t, tplane); + Node a_leq_av_or_b_geq_bv = nm->mkNode(OR, a_leq_av, b_geq_bv); + Node a_geq_av_or_b_leq_bv = nm->mkNode(OR, a_geq_av, b_leq_bv); + Node lb_reverse1 = + nm->mkNode(OR, t_geq_tplane.negate(), a_leq_av_or_b_geq_bv); + Trace("nl-ext-tplanes") + << "Tangent plane lemma (reverse) : " << lb_reverse1 + << std::endl; + lemmas.push_back(lb_reverse1); + Node lb_reverse2 = + nm->mkNode(OR, t_geq_tplane.negate(), a_geq_av_or_b_leq_bv); + Trace("nl-ext-tplanes") + << "Tangent plane lemma (reverse) : " << lb_reverse2 + << std::endl; + lemmas.push_back(lb_reverse2); } } } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index be87b7e8d..ac3bff21b 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -16,6 +16,8 @@ #include "theory/datatypes/datatypes_rewriter.h" +#include "expr/node_algorithm.h" + using namespace CVC4; using namespace CVC4::kind; @@ -115,8 +117,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) if (ev.getKind() == APPLY_CONSTRUCTOR) { Trace("dt-sygus-util") << "Rewrite " << in << " by unfolding...\n"; - const Datatype& dt = - static_cast<DatatypeType>(ev.getType().toType()).getDatatype(); + const Datatype& dt = ev.getType().getDatatype(); unsigned i = indexOf(ev.getOperator()); Node op = Node::fromExpr(dt[i].getSygusOp()); // if it is the "any constant" constructor, return its argument @@ -141,14 +142,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) children.push_back(nm->mkNode(DT_SYGUS_EVAL, cc)); } Node ret = mkSygusTerm(dt, i, children); - // if it is a variable, apply the substitution - if (ret.getKind() == BOUND_VARIABLE) - { - Assert(ret.hasAttribute(SygusVarNumAttribute())); - int vn = ret.getAttribute(SygusVarNumAttribute()); - Assert(Node::fromExpr(dt.getSygusVarList())[vn] == ret); - ret = args[vn]; - } + // apply the appropriate substitution + ret = applySygusArgs(dt, op, ret, args); Trace("dt-sygus-util") << "...got " << ret << "\n"; return RewriteResponse(REWRITE_AGAIN_FULL, ret); } @@ -186,6 +181,67 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_DONE, in); } +Node DatatypesRewriter::applySygusArgs(const Datatype& dt, + Node op, + Node n, + const std::vector<Node>& args) +{ + if (n.getKind() == BOUND_VARIABLE) + { + Assert(n.hasAttribute(SygusVarNumAttribute())); + int vn = n.getAttribute(SygusVarNumAttribute()); + Assert(Node::fromExpr(dt.getSygusVarList())[vn] == n); + return args[vn]; + } + // n is an application of operator op. + // We must compute the free variables in op to determine if there are + // any substitutions we need to make to n. + TNode val; + if (!op.hasAttribute(SygusVarFreeAttribute())) + { + std::unordered_set<Node, NodeHashFunction> fvs; + if (expr::getFreeVariables(op, fvs)) + { + if (fvs.size() == 1) + { + for (const Node& v : fvs) + { + val = v; + } + } + else + { + val = op; + } + } + Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl; + op.setAttribute(SygusVarFreeAttribute(), val); + } + else + { + val = op.getAttribute(SygusVarFreeAttribute()); + } + if (val.isNull()) + { + return n; + } + if (val.getKind() == BOUND_VARIABLE) + { + // single substitution case + int vn = val.getAttribute(SygusVarNumAttribute()); + TNode sub = args[vn]; + return n.substitute(val, sub); + } + // do the full substitution + std::vector<Node> vars; + Node bvl = Node::fromExpr(dt.getSygusVarList()); + for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++) + { + vars.push_back(bvl[i]); + } + return n.substitute(vars.begin(), vars.end(), args.begin(), args.end()); +} + Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op) { Assert(op.getKind() != BUILTIN); @@ -224,6 +280,13 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, Assert(!dt[i].getSygusOp().isNull()); std::vector<Node> schildren; Node op = Node::fromExpr(dt[i].getSygusOp()); + Trace("dt-sygus-util") << "Operator is " << op << std::endl; + if (children.empty()) + { + // no children, return immediately + Trace("dt-sygus-util") << "...return direct op" << std::endl; + return op; + } // if it is the any constant, we simply return the child if (op.getAttribute(SygusAnyConstAttribute())) { @@ -243,18 +306,13 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt, return ret; } Kind ok = NodeManager::operatorToKind(op); + Trace("dt-sygus-util") << "operator kind is " << ok << std::endl; if (ok != UNDEFINED_KIND) { - if (ok == APPLY_UF && schildren.size() == 1) - { - // This case is triggered for defined constant symbols. In this case, - // we return the operator itself instead of an APPLY_UF node. - ret = schildren[0]; - } - else - { - ret = NodeManager::currentNM()->mkNode(ok, schildren); - } + // If it is an APPLY_UF operator, we should have at least an operator and + // a child. + Assert(ok != APPLY_UF || schildren.size() != 1); + ret = NodeManager::currentNM()->mkNode(ok, schildren); Trace("dt-sygus-util") << "...return (op) " << ret << std::endl; return ret; } diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 6c1d64e5b..1a1735402 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -51,6 +51,28 @@ struct SygusSymBreakOkAttributeId typedef expr::Attribute<SygusSymBreakOkAttributeId, bool> SygusSymBreakOkAttribute; +/** sygus var free + * + * This attribute is used to mark whether sygus operators have free occurrences + * of variables from the formal argument list of the function-to-synthesize. + * + * We store three possible cases for sygus operators op: + * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null() + * In this case, op has no free variables from the formal argument list of the + * function-to-synthesize. + * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable. + * In this case, op has exactly one free variable, v. + * (3) op.getAttribute(SygusVarFreeAttribute())==op + * In this case, op has an arbitrary set (cardinality >1) of free variables from + * the formal argument list of the function to synthesize. + * + * This attribute is used to compute applySygusArgs below. + */ +struct SygusVarFreeAttributeId +{ +}; +typedef expr::Attribute<SygusVarFreeAttributeId, Node> SygusVarFreeAttribute; + namespace datatypes { class DatatypesRewriter { @@ -150,6 +172,37 @@ public: unsigned i, const std::vector<Node>& children); /** + * n is a builtin term that is an application of operator op. + * + * This returns an n' such that (eval n args) is n', where n' is a instance of + * n for the appropriate substitution. + * + * For example, given a function-to-synthesize with formal argument list (x,y), + * say we have grammar: + * A -> A+A | A+x | A+(x+y) | y + * These lead to constructors with sygus ops: + * C1 / (lambda w1 w2. w1+w2) + * C2 / (lambda w1. w1+x) + * C3 / (lambda w1. w1+(x+y)) + * C4 / y + * Examples of calling this function: + * applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } ) + * ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2). + * applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } ) + * ... returns (APPLY_UF (lambda w1. w1+3) t1). + * applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } ) + * ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1). + * applySygusArgs( dt, C4, y, { 3, 5 } ) + * ... returns 5. + * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4, + * to cache the results of whether the evaluation of this constructor needs + * a substitution over the formal argument list of the function-to-synthesize. + */ + static Node applySygusArgs(const Datatype& dt, + Node op, + Node n, + const std::vector<Node>& args); + /** * Get the builtin sygus operator for constructor term n of sygus datatype * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus * constructor whose sygus op is the builtin operator +, this method returns +. diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index dc18a2005..07f754810 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -561,7 +561,9 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false; } -bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) { +bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, + std::vector<Node>& terms) +{ if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected if (p->atConflictEffort()) { @@ -571,12 +573,14 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node Trace("qcf-instance-check") << " " << terms[i] << std::endl; subs[d_q[0][i]] = terms[i]; } + TermDb* tdb = p->getTermDatabase(); for( unsigned i=0; i<d_extra_var.size(); i++ ){ Node n = getCurrentExpValue( d_extra_var[i] ); Trace("qcf-instance-check") << " " << d_extra_var[i] << " -> " << n << std::endl; subs[d_extra_var[i]] = n; } - if( !p->getTermDatabase()->isEntailed( d_q[1], subs, false, false ) ){ + if (!tdb->isEntailed(d_q[1], subs, false, false)) + { Trace("qcf-instance-check") << "...not entailed to be false." << std::endl; return true; } @@ -1822,8 +1826,9 @@ QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c) d_conflict(c, false), d_true(NodeManager::currentNM()->mkConst<bool>(true)), d_false(NodeManager::currentNM()->mkConst<bool>(false)), - d_effort(EFFORT_INVALID), - d_needs_computeRelEqr() {} + d_effort(EFFORT_INVALID) +{ +} //-------------------------------------------------- registration @@ -1892,7 +1897,25 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) { } void QuantConflictFind::reset_round( Theory::Effort level ) { - d_needs_computeRelEqr = true; + Trace("qcf-check") << "QuantConflictFind::reset_round" << std::endl; + Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl; + d_eqcs.clear(); + + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(getEqualityEngine()); + TermDb* tdb = getTermDatabase(); + while (!eqcs_i.isFinished()) + { + Node r = (*eqcs_i); + if (tdb->hasTermCurrent(r)) + { + TypeNode rtn = r.getType(); + if (!options::cbqi() || !TermUtil::hasInstConstAttr(r)) + { + d_eqcs[rtn].push_back(r); + } + } + ++eqcs_i; + } } void QuantConflictFind::setIrrelevantFunction( TNode f ) { @@ -1928,182 +1951,240 @@ inline QuantConflictFind::Effort QcfEffortEnd() { void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) { CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time); - if (quant_e == QEFFORT_CONFLICT) + if (quant_e != QEFFORT_CONFLICT) { - Trace("qcf-check") << "QCF : check : " << level << std::endl; - if( d_conflict ){ - Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl; - if( level>=Theory::EFFORT_FULL ){ - Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl; - //Assert( false ); - } - }else{ - int addedLemmas = 0; - ++(d_statistics.d_inst_rounds); - double clSet = 0; - int prevEt = 0; - if( Trace.isOn("qcf-engine") ){ - prevEt = d_statistics.d_entailment_checks.getData(); - clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl; - } - computeRelevantEqr(); - - d_irr_func.clear(); - d_irr_quant.clear(); - - if( Trace.isOn("qcf-debug") ){ - Trace("qcf-debug") << std::endl; - debugPrint("qcf-debug"); - Trace("qcf-debug") << std::endl; - } - bool isConflict = false; - for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) { - d_effort = static_cast<Effort>(e); - Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; - for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true ); - if( d_quantEngine->hasOwnership( q, this ) && d_irr_quant.find( q )==d_irr_quant.end() ){ - QuantInfo * qi = &d_qinfo[q]; - - Assert( d_qinfo.find( q )!=d_qinfo.end() ); - if( qi->matchGeneratorIsValid() ){ - Trace("qcf-check") << "Check quantified formula "; - debugPrintQuant("qcf-check", q); - Trace("qcf-check") << " : " << q << "..." << std::endl; - - Trace("qcf-check-debug") << "Reset round..." << std::endl; - if( qi->reset_round( this ) ){ - //try to make a matches making the body false - Trace("qcf-check-debug") << "Get next match..." << std::endl; - while( qi->getNextMatch( this ) ){ - if( d_quantEngine->inConflict() ){ - Trace("qcf-check") << " ... Quantifiers engine discovered conflict, "; - Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl; - break; - }else{ - Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - qi->getMatch( terms ); - bool tcs = qi->isTConstraintSpurious( this, terms ); - if( !tcs ){ - //for debugging - if( Debug.isOn("qcf-check-inst") ){ - Node inst = d_quantEngine->getInstantiate() - ->getInstantiation(q, terms); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( !getTermDatabase()->isEntailed( inst, true ) ); - Assert(getTermDatabase()->isEntailed(inst, false) || - e > EFFORT_CONFLICT); - } - if (d_quantEngine->getInstantiate()->addInstantiation( - q, terms)) - { - Trace("qcf-check") << " ... Added instantiation" << std::endl; - Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-inst"); - Trace("qcf-inst") << std::endl; - ++addedLemmas; - if (e == EFFORT_CONFLICT) { - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); - if( options::qcfAllConflict() ){ - isConflict = true; - }else{ - d_conflict.set( true ); - } - break; - } else if (e == EFFORT_PROP_EQ) { - d_quantEngine->markRelevant( q ); - ++(d_quantEngine->d_statistics.d_instantiations_qcf); - } - }else{ - Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; - //this should only happen if the algorithm generates the same propagating instance twice this round - //in this case, break to avoid exponential behavior - break; - } - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is T-inconsistent)" << std::endl; - } - //clean up assigned - qi->revertMatch( this, assigned ); - d_tempCache.clear(); - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; - } - }else{ - Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl; - } - } - } - Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; - } - if (d_conflict || d_quantEngine->inConflict()) - { - break; - } - } - } - } - if( addedLemmas>0 || d_quantEngine->inConflict() ){ + return; + } + Trace("qcf-check") << "QCF : check : " << level << std::endl; + if (d_conflict) + { + Trace("qcf-check2") << "QCF : finished check : already in conflict." + << std::endl; + if (level >= Theory::EFFORT_FULL) + { + Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl; + } + return; + } + unsigned addedLemmas = 0; + ++(d_statistics.d_inst_rounds); + double clSet = 0; + int prevEt = 0; + if (Trace.isOn("qcf-engine")) + { + prevEt = d_statistics.d_entailment_checks.getData(); + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level + << "---" << std::endl; + } + + // reset the round-specific information + d_irr_func.clear(); + d_irr_quant.clear(); + + if (Trace.isOn("qcf-debug")) + { + Trace("qcf-debug") << std::endl; + debugPrint("qcf-debug"); + Trace("qcf-debug") << std::endl; + } + bool isConflict = false; + FirstOrderModel* fm = d_quantEngine->getModel(); + unsigned nquant = fm->getNumAssertedQuantifiers(); + // for each effort level (find conflict, find propagating) + for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) + { + // set the effort (data member for convienence of access) + d_effort = static_cast<Effort>(e); + Trace("qcf-check") << "Checking quantified formulas at effort " << e + << "..." << std::endl; + // for each quantified formula + for (unsigned i = 0; i < nquant; i++) + { + Node q = fm->getAssertedQuantifier(i, true); + if (d_quantEngine->hasOwnership(q, this) + && d_irr_quant.find(q) == d_irr_quant.end() + && fm->isQuantifierActive(q)) + { + // check this quantified formula + checkQuantifiedFormula(q, isConflict, addedLemmas); + if (d_conflict || d_quantEngine->inConflict()) + { break; } } - if( isConflict ){ - d_conflict.set( true ); - } - if( Trace.isOn("qcf-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet); - if( addedLemmas>0 ){ - Trace("qcf-engine") - << ", effort = " - << (d_effort == EFFORT_CONFLICT - ? "conflict" - : (d_effort == EFFORT_PROP_EQ ? "prop_eq" : "mc")); - Trace("qcf-engine") << ", addedLemmas = " << addedLemmas; - } - Trace("qcf-engine") << std::endl; - int currEt = d_statistics.d_entailment_checks.getData(); - if( currEt!=prevEt ){ - Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl; - } - } - Trace("qcf-check2") << "QCF : finished check : " << level << std::endl; } + // We are done if we added a lemma, or discovered a conflict in another + // way. An example of the latter case is when two disequal congruent terms + // are discovered during term indexing. + if (addedLemmas > 0 || d_quantEngine->inConflict()) + { + break; + } + } + if (isConflict) + { + d_conflict.set(true); } + if (Trace.isOn("qcf-engine")) + { + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("qcf-engine") << "Finished conflict find engine, time = " + << (clSet2 - clSet); + if (addedLemmas > 0) + { + Trace("qcf-engine") << ", effort = " + << (d_effort == EFFORT_CONFLICT + ? "conflict" + : (d_effort == EFFORT_PROP_EQ ? "prop_eq" + : "mc")); + Trace("qcf-engine") << ", addedLemmas = " << addedLemmas; + } + Trace("qcf-engine") << std::endl; + int currEt = d_statistics.d_entailment_checks.getData(); + if (currEt != prevEt) + { + Trace("qcf-engine") << " Entailment checks = " << (currEt - prevEt) + << std::endl; + } + } + Trace("qcf-check2") << "QCF : finished check : " << level << std::endl; } -void QuantConflictFind::computeRelevantEqr() { - if( d_needs_computeRelEqr ){ - d_needs_computeRelEqr = false; - Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl; - d_eqcs.clear(); - - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); - while( !eqcs_i.isFinished() ){ - Node r = (*eqcs_i); - if( getTermDatabase()->hasTermCurrent( r ) ){ - TypeNode rtn = r.getType(); - if( !options::cbqi() || !TermUtil::hasInstConstAttr( r ) ){ - d_eqcs[rtn].push_back( r ); +void QuantConflictFind::checkQuantifiedFormula(Node q, + bool& isConflict, + unsigned& addedLemmas) +{ + QuantInfo* qi = &d_qinfo[q]; + Assert(d_qinfo.find(q) != d_qinfo.end()); + if (!qi->matchGeneratorIsValid()) + { + // quantified formula is not properly set up for matching + return; + } + if (Trace.isOn("qcf-check")) + { + Trace("qcf-check") << "Check quantified formula "; + debugPrintQuant("qcf-check", q); + Trace("qcf-check") << " : " << q << "..." << std::endl; + } + + Trace("qcf-check-debug") << "Reset round..." << std::endl; + if (!qi->reset_round(this)) + { + // it is typically the case that another conflict (e.g. in the term + // database) was discovered if we fail here. + return; + } + // try to make a matches making the body false or propagating + Trace("qcf-check-debug") << "Get next match..." << std::endl; + Instantiate* qinst = d_quantEngine->getInstantiate(); + while (qi->getNextMatch(this)) + { + if (d_quantEngine->inConflict()) + { + Trace("qcf-check") << " ... Quantifiers engine discovered conflict, "; + Trace("qcf-check") << "probably related to disequal congruent terms in " + "master equality engine" + << std::endl; + return; + } + if (Trace.isOn("qcf-inst")) + { + Trace("qcf-inst") << "*** Produced match at effort " << d_effort << " : " + << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + } + // check whether internal match constraints are satisfied + if (qi->isMatchSpurious(this)) + { + Trace("qcf-inst") << " ... Spurious (match is inconsistent)" + << std::endl; + continue; + } + // check whether match can be completed + std::vector<int> assigned; + if (!qi->completeMatch(this, assigned)) + { + Trace("qcf-inst") << " ... Spurious (cannot assign unassigned vars)" + << std::endl; + continue; + } + // check whether the match is spurious according to (T-)entailment checks + std::vector<Node> terms; + qi->getMatch(terms); + bool tcs = qi->isTConstraintSpurious(this, terms); + if (tcs) + { + Trace("qcf-inst") << " ... Spurious (match is T-inconsistent)" + << std::endl; + } + else + { + // otherwise, we have a conflict/propagating instance + // for debugging + if (Debug.isOn("qcf-check-inst")) + { + Node inst = qinst->getInstantiation(q, terms); + Debug("qcf-check-inst") + << "Check instantiation " << inst << "..." << std::endl; + Assert(!getTermDatabase()->isEntailed(inst, true)); + Assert(getTermDatabase()->isEntailed(inst, false) + || d_effort > EFFORT_CONFLICT); + } + // Process the lemma: either add an instantiation or specific lemmas + // constructed during the isTConstraintSpurious call, or both. + if (!qinst->addInstantiation(q, terms)) + { + Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl; + // This should only happen if the algorithm generates the same + // propagating instance twice this round. In this case, return + // to avoid exponential behavior. + return; + } + Trace("qcf-check") << " ... Added instantiation" << std::endl; + if (Trace.isOn("qcf-inst")) + { + Trace("qcf-inst") << "*** Was from effort " << d_effort << " : " + << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + } + ++addedLemmas; + if (d_effort == EFFORT_CONFLICT) + { + // mark relevant: this ensures that quantified formula q is + // checked first on the next round. This is an optimization to + // ensure that quantified formulas that are more likely to have + // conflicting instances are checked earlier. + d_quantEngine->markRelevant(q); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); + if (options::qcfAllConflict()) + { + isConflict = true; + } + else + { + d_conflict.set(true); } + return; + } + else if (d_effort == EFFORT_PROP_EQ) + { + d_quantEngine->markRelevant(q); + ++(d_quantEngine->d_statistics.d_instantiations_qcf); } - ++eqcs_i; } + // clean up assigned + qi->revertMatch(this, assigned); + d_tempCache.clear(); } + Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl; } - //-------------------------------------------------- debugging - void QuantConflictFind::debugPrint( const char * c ) { //print the equivalance classes Trace(c) << "----------EQ classes" << std::endl; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index f22910191..7e4eb517d 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -242,14 +242,30 @@ public: bool needsCheck(Theory::Effort level) override; /** reset round */ void reset_round(Theory::Effort level) override; - /** check */ + /** check + * + * This method attempts to construct a conflicting or propagating instance. + * If such an instance exists, then it makes a call to + * Instantiation::addInstantiation or QuantifiersEngine::addLemma. + */ void check(Theory::Effort level, QEffort quant_e) override; private: - bool d_needs_computeRelEqr; -public: - void computeRelevantEqr(); -private: + /** check quantified formula + * + * This method is called by the above check method for each quantified + * formula q. It attempts to find a conflicting or propagating instance for + * q, depending on the effort level (d_effort). + * + * isConflict: this is set to true if we discovered a conflicting instance. + * This flag may be set instead of d_conflict if --qcf-all-conflict is true, + * in which we continuing adding all conflicts. + * addedLemmas: tracks the total number of lemmas added, and is incremented by + * this method when applicable. + */ + void checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas); + + private: void debugPrint( const char * c ); //for debugging std::vector< Node > d_quants; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index ff42a9c89..d92f36afb 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -119,7 +119,6 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { QuantConflictFind * qcf = d_quantEngine->getConflictFind(); if( qcf ){ //reset QCF module - qcf->computeRelevantEqr(); qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); //get the proper quantifiers info std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f ); diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index e44b604d0..7324add50 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -133,7 +133,18 @@ void SygusEvalUnfold::registerModelValue(Node a, bool do_unfold = false; if (options::sygusEvalUnfoldBool()) { - if (bTerm.getKind() == ITE || bTerm.getType().isBoolean()) + Node bTermUse = bTerm; + if (bTerm.getKind() == APPLY_UF) + { + // if the builtin term is non-beta-reduced application of lambda, + // we look at the body of the lambda. + Node bTermOp = bTerm.getOperator(); + if (bTermOp.getKind() == LAMBDA) + { + bTermUse = bTermOp[0]; + } + } + if (bTermUse.getKind() == ITE || bTermUse.getType().isBoolean()) { do_unfold = true; } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 48da8e8e8..263c88d15 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -712,7 +712,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) { Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl; - ops[i].push_back( dt[k].getConstructor() ); + Expr cop = dt[k].getConstructor(); + if (dt[k].getNumArgs() == 0) + { + // Nullary constructors are interpreted as terms, not operators. + // Thus, we apply them to no arguments here. + cop = nm->mkNode(APPLY_CONSTRUCTOR, Node::fromExpr(cop)).toExpr(); + } + ops[i].push_back(cop); cnames[i].push_back(dt[k].getName()); cargs[i].push_back(std::vector<Type>()); Trace("sygus-grammar-def") << "...add for selectors" << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 6ad590f28..2b2c87f38 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -43,7 +43,6 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn) std::map<int, Node> pre; Node g = tds->mkGeneric(dt, i, pre); Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl; - Assert(g.getNumChildren() == dt[i].getNumArgs()); d_gen_terms[i] = g; for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) { diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index af820b0fc..01d08dad8 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -411,6 +411,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { Trace("sygus-db") << ", kind = " << sk; d_kinds[tn][sk] = i; d_arg_kind[tn][i] = sk; + if (sk == ITE) + { + // mark that this type has an ITE + d_hasIte[tn] = true; + } } else if (sop.isConst() && dt[i].getNumArgs() == 0) { @@ -432,6 +437,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { << ", argument to a lambda constructor is not " << lat << std::endl; } + if (sop[0].getKind() == ITE) + { + // mark that this type has an ITE + d_hasIte[tn] = true; + } } // symbolic constructors if (n.getAttribute(SygusAnyConstAttribute())) @@ -602,7 +612,7 @@ void TermDbSygus::registerEnumerator(Node e, // solution" clauses. const Datatype& dt = et.getDatatype(); if (options::sygusStream() - || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean())) + || (!hasIte(et) && !dt.getSygusType().isBoolean())) { isActiveGen = true; } @@ -1003,6 +1013,10 @@ int TermDbSygus::getOpConsNum( TypeNode tn, Node n ) { bool TermDbSygus::hasKind( TypeNode tn, Kind k ) { return getKindConsNum( tn, k )!=-1; } +bool TermDbSygus::hasIte(TypeNode tn) const +{ + return d_hasIte.find(tn) != d_hasIte.end(); +} bool TermDbSygus::hasConst( TypeNode tn, Node n ) { return getConstConsNum( tn, n )!=-1; } @@ -1502,14 +1516,9 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc); } Node ret = mkGeneric(dt, i, pre); - // if it is a variable, apply the substitution - if (ret.getKind() == kind::BOUND_VARIABLE) - { - Assert(ret.hasAttribute(SygusVarNumAttribute())); - int i = ret.getAttribute(SygusVarNumAttribute()); - Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret); - return args[i]; - } + // apply the appropriate substitution to ret + ret = datatypes::DatatypesRewriter::applySygusArgs(dt, sop, ret, args); + // rewrite ret = Rewriter::rewrite(ret); return ret; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 0f3d650d3..2854ecab6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -393,6 +393,11 @@ class TermDbSygus { std::map<TypeNode, std::vector<Node> > d_var_list; std::map<TypeNode, std::map<int, Kind> > d_arg_kind; std::map<TypeNode, std::map<Kind, int> > d_kinds; + /** + * Whether this sygus type has a constructors whose sygus operator is ITE, + * or is a lambda whose body is ITE. + */ + std::map<TypeNode, bool> d_hasIte; std::map<TypeNode, std::map<int, Node> > d_arg_const; std::map<TypeNode, std::map<Node, int> > d_consts; std::map<TypeNode, std::map<Node, int> > d_ops; @@ -462,6 +467,11 @@ class TermDbSygus { int getConstConsNum( TypeNode tn, Node n ); int getOpConsNum( TypeNode tn, Node n ); bool hasKind( TypeNode tn, Kind k ); + /** + * Returns true if this sygus type has a constructors whose sygus operator is + * ITE, or is a lambda whose body is ITE. + */ + bool hasIte(TypeNode tn) const; bool hasConst( TypeNode tn, Node n ); bool hasOp( TypeNode tn, Node n ); Node getConsNumConst( TypeNode tn, int i ); diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 91beb1ab5..0360228c6 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -20,6 +20,9 @@ #include "options/strings_options.h" #include "theory/strings/theory_strings_rewriter.h" +using namespace CVC4; +using namespace CVC4::kind; + namespace CVC4 { namespace theory { namespace strings { @@ -808,39 +811,72 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes break; } case kind::REGEXP_CONCAT: { - //TODO: rewrite empty - Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); - Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); - Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); - Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero), - NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) ); - Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, d_zero, b1)); - Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1))); - Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate(); - if(r[0].getKind() == kind::STRING_TO_REGEXP) { - s1r1 = s1.eqNode(r[0][0]).negate(); - } else if(r[0].getKind() == kind::REGEXP_EMPTY) { - s1r1 = d_true; + // The following simplification states that + // ~( s in R1 ++ R2 ) + // is equivalent to + // forall x. + // 0 <= x <= len(s) => + // ~( substr(s,0,x) in R1 ) OR ~( substr(s,x,len(s)-x) in R2) + Node lens = nm->mkNode(STRING_LENGTH, s); + // the index we are removing from the RE concatenation + unsigned indexRm = 0; + Node b1; + Node b1v; + // As an optimization to the above reduction, if we can determine that + // all strings in the language of R1 have the same length, say n, + // then the conclusion of the reduction is quantifier-free: + // ~( substr(s,0,n) in R1 ) OR ~( substr(s,n,len(s)-n) in R2) + Node reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[0]); + if (reLength.isNull()) + { + // try from the opposite end + unsigned indexE = r.getNumChildren() - 1; + reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[indexE]); + if (!reLength.isNull()) + { + indexRm = indexE; + } + } + Node guard; + if (reLength.isNull()) + { + b1 = nm->mkBoundVar(nm->integerType()); + b1v = nm->mkNode(BOUND_VAR_LIST, b1); + guard = nm->mkNode(AND, + nm->mkNode(GEQ, b1, d_zero), + nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, s), b1)); + } + else + { + b1 = reLength; + } + Node s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1); + Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1)); + if (indexRm != 0) + { + // swap if we are removing from the end + Node sswap = s1; + s1 = s2; + s2 = sswap; } - Node r2 = r[1]; - if(r.getNumChildren() > 2) { - std::vector< Node > nvec; - for(unsigned i=1; i<r.getNumChildren(); i++) { + Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[indexRm]).negate(); + std::vector<Node> nvec; + for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; i++) + { + if (i != indexRm) + { nvec.push_back( r[i] ); } - r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, nvec); } + Node r2 = nvec.size() == 1 ? nvec[0] : nm->mkNode(REGEXP_CONCAT, nvec); r2 = Rewriter::rewrite(r2); - Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r2).negate(); - if(r2.getKind() == kind::STRING_TO_REGEXP) { - s2r2 = s2.eqNode(r2[0]).negate(); - } else if(r2.getKind() == kind::REGEXP_EMPTY) { - s2r2 = d_true; + Node s2r2 = nm->mkNode(STRING_IN_REGEXP, s2, r2).negate(); + conc = nm->mkNode(OR, s1r1, s2r2); + if (!b1v.isNull()) + { + conc = nm->mkNode(OR, guard.negate(), conc); + conc = nm->mkNode(FORALL, b1v, conc); } - - conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2); - conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc); - conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc); break; } case kind::REGEXP_UNION: { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c7f7c5c99..0883eebfa 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4475,19 +4475,29 @@ void TheoryStrings::checkNormalFormsDeq() for( unsigned j=0; j<cols[i].size(); j++ ){ for( unsigned k=(j+1); k<cols[i].size(); k++ ){ //for strings that are disequal, but have the same length - if( areDisequal( cols[i][j], cols[i][k] ) ){ - Assert( !d_conflict ); - if (Trace.isOn("strings-solve")) + if (cols[i][j].isConst() && cols[i][k].isConst()) + { + // if both are constants, they should be distinct, and its trivial + Assert(cols[i][j] != cols[i][k]); + } + else + { + if (areDisequal(cols[i][j], cols[i][k])) { - Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); - Trace("strings-solve") << " against " << cols[i][k] << " "; - printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); - Trace("strings-solve") << "..." << std::endl; - } - processDeq( cols[i][j], cols[i][k] ); - if( hasProcessed() ){ - return; + Assert(!d_conflict); + if (Trace.isOn("strings-solve")) + { + Trace("strings-solve") << "- Compare " << cols[i][j] << " "; + printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve"); + Trace("strings-solve") << " against " << cols[i][k] << " "; + printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve"); + Trace("strings-solve") << "..." << std::endl; + } + processDeq(cols[i][j], cols[i][k]); + if (hasProcessed()) + { + return; + } } } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2ec8b26c9..fe059e663 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1573,6 +1573,7 @@ set(regress_1_tests regress1/strings/re-agg-total1.smt2 regress1/strings/re-agg-total2.smt2 regress1/strings/re-elim-exact.smt2 + regress1/strings/re-neg-concat-reduct.smt2 regress1/strings/re-unsound-080718.smt2 regress1/strings/regexp001.smt2 regress1/strings/regexp002.smt2 diff --git a/test/regress/regress1/strings/re-neg-concat-reduct.smt2 b/test/regress/regress1/strings/re-neg-concat-reduct.smt2 new file mode 100644 index 000000000..cbe8c4a8b --- /dev/null +++ b/test/regress/regress1/strings/re-neg-concat-reduct.smt2 @@ -0,0 +1,12 @@ +(set-info :smt-lib-version 2.5) +(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun x () String) + +(assert (not (= x ""))) +(assert (not (str.in.re x (re.++ (str.to.re "AB") (re.* (str.to.re "A")))))) +(assert (not (str.in.re x (re.++ (re.* (str.to.re "A")) (str.to.re "B"))))) + +(check-sat) diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy index 2f3f4dbb9..336c59b27 100644 --- a/test/regress/regress1/sygus/sygus-dt.sy +++ b/test/regress/regress1/sygus/sygus-dt.sy @@ -7,7 +7,7 @@ (define-fun g ((x Int)) List (cons (+ x 1) nil)) (define-fun i () List (cons 3 nil)) -(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) (nil) (tail Start))) +(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start))) (StartInt Int (x 0 1 (+ StartInt StartInt))))) (declare-var x Int) diff --git a/test/regress/regress2/strings/norn-dis-0707-3.smt2 b/test/regress/regress2/strings/norn-dis-0707-3.smt2 index bc0f877ad..47b2e6b19 100644 --- a/test/regress/regress2/strings/norn-dis-0707-3.smt2 +++ b/test/regress/regress2/strings/norn-dis-0707-3.smt2 @@ -1,6 +1,7 @@ (set-logic QF_S) (set-info :status sat) (set-option :strings-exp true) +(set-option :strings-fmf true) (declare-fun var_0 () String) (declare-fun var_1 () String) |