diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/cvc/Cvc.g | 2 | ||||
-rw-r--r-- | src/parser/parser.cpp | 20 | ||||
-rw-r--r-- | src/parser/parser.h | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 11 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 16 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 17 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 1 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_utilities.cpp | 9 | ||||
-rw-r--r-- | src/theory/arith/nl_model.cpp | 25 | ||||
-rw-r--r-- | src/theory/arith/nl_model.h | 9 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 290 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 59 | ||||
-rw-r--r-- | src/theory/strings/core_solver.cpp | 82 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 42 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/word.cpp | 28 | ||||
-rw-r--r-- | src/theory/strings/word.h | 16 | ||||
-rw-r--r-- | src/util/regexp.cpp | 8 | ||||
-rw-r--r-- | src/util/regexp.h | 14 |
21 files changed, 391 insertions, 274 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 64eb56c74..abfd363f8 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2331,7 +2331,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] )* RBRACKET )? { - datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), + datatypes.push_back(Datatype(SOLVER->getExprManager(), id, api::sortVectorToTypes(params), false)); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 87fa93dcc..e9a037d6e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -76,11 +76,6 @@ Parser::~Parser() { delete d_input; } -ExprManager* Parser::getExprManager() const -{ - return d_solver->getExprManager(); -} - api::Solver* Parser::getSolver() const { return d_solver; } api::Term Parser::getSymbol(const std::string& name, SymbolType type) @@ -339,7 +334,7 @@ void Parser::defineParameterizedType(const std::string& name, api::Sort Parser::mkSort(const std::string& name, uint32_t flags) { Debug("parser") << "newSort(" << name << ")" << std::endl; - api::Sort type = getExprManager()->mkSort(name, flags); + api::Sort type = d_solver->getExprManager()->mkSort(name, flags); defineType( name, type, @@ -353,7 +348,8 @@ api::Sort Parser::mkSortConstructor(const std::string& name, { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = getExprManager()->mkSortConstructor(name, arity, flags); + api::Sort type = + d_solver->getExprManager()->mkSortConstructor(name, arity, flags); defineType( name, vector<api::Sort>(arity), @@ -383,7 +379,7 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = getExprManager()->mkSortConstructor( + api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor( name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); defineType(name, params, unresolved); api::Sort t = getSort(name, params); @@ -404,7 +400,8 @@ std::vector<api::Sort> Parser::mkMutualDatatypeTypes( try { std::set<Type> tset = api::sortSetToTypes(d_unresolved); std::vector<DatatypeType> dtypes = - getExprManager()->mkMutualDatatypeTypes(datatypes, tset, flags); + d_solver->getExprManager()->mkMutualDatatypeTypes( + datatypes, tset, flags); std::vector<api::Sort> types; for (unsigned i = 0, dtsize = dtypes.size(); i < dtsize; i++) { @@ -593,7 +590,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) // parametric datatype. if (s.isParametricDatatype()) { - ExprManager* em = getExprManager(); + ExprManager* em = d_solver->getExprManager(); // apply type ascription to the operator Expr e = t.getExpr(); const DatatypeConstructor& dtc = @@ -633,7 +630,8 @@ api::Term Parser::mkVar(const std::string& name, const api::Sort& type, uint32_t flags) { - return api::Term(getExprManager()->mkVar(name, type.getType(), flags)); + return api::Term( + d_solver->getExprManager()->mkVar(name, type.getType(), flags)); } //!!!!!!!!!!! temporary diff --git a/src/parser/parser.h b/src/parser/parser.h index c7efcbacb..1197c1ff6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -265,9 +265,6 @@ public: virtual ~Parser(); - /** Get the associated <code>ExprManager</code>. */ - ExprManager* getExprManager() const; - /** Get the associated solver. */ api::Solver* getSolver() const; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index aa62eab5d..d87c44a68 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -959,7 +959,7 @@ sygusGrammar[CVC4::api::Sort & ret, Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl; // make the datatype, which encodes terms generated by this non-terminal std::string dname = i.first; - datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), dname)); + datatypes.push_back(Datatype(SOLVER->getExprManager(), dname)); // make its unresolved type, used for referencing the final version of // the datatype PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); @@ -1537,7 +1537,7 @@ datatypesDef[bool isCo, PARSER_STATE->parseError("Wrong number of parameters for datatype."); } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; - dts.push_back(Datatype(PARSER_STATE->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo)); + dts.push_back(Datatype(SOLVER->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo)); } LPAREN_TOK ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+ @@ -1547,7 +1547,7 @@ datatypesDef[bool isCo, PARSER_STATE->parseError("No parameters given for datatype."); } Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl; - dts.push_back(Datatype(PARSER_STATE->getExprManager(), + dts.push_back(Datatype(SOLVER->getExprManager(), dnames[dts.size()], api::sortVectorToTypes(params), isCo)); @@ -2532,7 +2532,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, * below. */ : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); } { - datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), + datatypes.push_back(Datatype(SOLVER->getExprManager(), id, api::sortVectorToTypes(params), isCo)); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2df73d9e4..c0484e52b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1112,7 +1112,7 @@ bool Smt2::pushSygusDatatypeDef( std::vector<std::vector<std::string>>& unresolved_gterm_sym) { sorts.push_back(t); - datatypes.push_back(Datatype(getExprManager(), dname)); + datatypes.push_back(Datatype(d_solver->getExprManager(), dname)); ops.push_back(std::vector<ParseOp>()); cnames.push_back(std::vector<std::string>()); cargs.push_back(std::vector<std::vector<api::Sort>>()); @@ -1573,7 +1573,7 @@ void Smt2::addSygusConstructorVariables(Datatype& dt, InputLanguage Smt2::getLanguage() const { - return getExprManager()->getOptions().getInputLanguage(); + return d_solver->getExprManager()->getOptions().getInputLanguage(); } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) @@ -1746,7 +1746,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } } // Second phase: apply the arguments to the parse op - ExprManager* em = getExprManager(); + const Options& opts = d_solver->getExprManager()->getOptions(); // handle special cases if (p.d_kind == api::STORE_ALL && !p.d_type.isNull()) { @@ -1842,8 +1842,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) else if (isBuiltinOperator) { Trace("ajr-temp") << "mkTerm builtin operator" << std::endl; - if (!em->getOptions().getUfHo() - && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); @@ -1884,7 +1883,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!em->getOptions().getUfHo()) + if (!opts.getUfHo()) { parseError("Cannot partially apply functions unless --uf-ho is set."); } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index a21cc6785..51b852eac 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -69,20 +69,19 @@ Tptp::~Tptp() { } void Tptp::addTheory(Theory theory) { - ExprManager * em = getExprManager(); switch(theory) { case THEORY_CORE: //TPTP (CNF and FOF) is unsorted so we define this common type { std::string d_unsorted_name = "$$unsorted"; - d_unsorted = api::Sort(em->mkSort(d_unsorted_name)); + d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name); preemptCommand( new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType())); } // propositionnal - defineType("Bool", em->booleanType()); - defineVar("$true", em->mkConst(true)); - defineVar("$false", em->mkConst(false)); + defineType("Bool", d_solver->getBooleanSort()); + defineVar("$true", d_solver->mkTrue()); + defineVar("$false", d_solver->mkFalse()); addOperator(api::AND); addOperator(api::EQUAL); addOperator(api::IMPLIES); @@ -312,12 +311,11 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) isBuiltinKind = true; } assert(kind != api::NULL_EXPR); - ExprManager* em = getExprManager(); + const Options& opts = d_solver->getExprManager()->getOptions(); // Second phase: apply parse op to the arguments if (isBuiltinKind) { - if (!em->getOptions().getUfHo() - && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT)) { // need --uf-ho if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); @@ -352,7 +350,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!em->getOptions().getUfHo()) + if (!opts.getUfHo()) { parseError("Cannot partially apply functions unless --uf-ho is set."); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 86dd31da2..79a8904cd 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1174,6 +1174,23 @@ void DeclareFunctionCommandToStream(std::ostream& out, } // namespace +void CvcPrinter::toStream(std::ostream& out, const Model& m) const +{ + // print the model comments + std::stringstream c; + m.getComments(c); + std::string ln; + while (std::getline(c, ln)) + { + out << "; " << ln << std::endl; + } + + // print the model + out << "MODEL BEGIN" << std::endl; + this->Printer::toStream(out, m); + out << "MODEL END;" << std::endl; +} + void CvcPrinter::toStream(std::ostream& out, const Model& model, const Command* command) const diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index d379af7e3..1694ea1ec 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -42,6 +42,7 @@ class CvcPrinter : public CVC4::Printer { bool types, size_t dag) const override; void toStream(std::ostream& out, const CommandStatus* s) const override; + void toStream(std::ostream& out, const Model& m) const override; private: void toStream( diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 4f93ba745..222b63db5 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -753,7 +753,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL) ? nm->mkNode(kind::UMINUS, nn) : nn; - return RewriteResponse(REWRITE_AGAIN, ret); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); } else if (dIsConstant && n.getKind() == kind::CONST_RATIONAL) { diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 65aaceb80..cbb27197f 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -224,10 +224,13 @@ Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs) else { TheoryId ctid = theory::kindToTheoryId(ck); - if (ctid != THEORY_ARITH && ctid != THEORY_BOOL - && ctid != THEORY_BUILTIN) + if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL + && ctid != THEORY_BUILTIN) + || isTranscendentalKind(ck)) { - // do not traverse beneath applications that belong to another theory + // Do not traverse beneath applications that belong to another theory + // besides (core) arithmetic. Notice that transcendental function + // applications are also not traversed here. visited[cur] = cur; } else diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index d09a138fe..904300004 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -1208,31 +1208,6 @@ bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol) return comp == d_true; } -bool NlModel::isRefineableTfFun(Node tf) -{ - Assert(tf.getKind() == SINE || tf.getKind() == EXPONENTIAL); - if (tf.getKind() == SINE) - { - // we do not consider e.g. sin( -1*x ), since considering sin( x ) will - // have the same effect. We also do not consider sin(x+y) since this is - // handled by introducing a fresh variable (see the map d_tr_base in - // NonlinearExtension). - if (!tf[0].isVar()) - { - return false; - } - } - // Figure 3 : c - Node c = computeAbstractModelValue(tf[0]); - Assert(c.isConst()); - int csign = c.getConst<Rational>().sgn(); - if (csign == 0) - { - return false; - } - return true; -} - bool NlModel::getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter) const { Assert(c.isConst()); diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h index a8746ca2e..5129a7a32 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl_model.h @@ -256,15 +256,6 @@ class NlModel bool simpleCheckModelLit(Node lit); bool simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol); //---------------------------end check model - - /** is refinable transcendental function - * - * A transcendental function application is not refineable if its current - * model value is zero, or if it is an application of SINE applied - * to a non-variable. - */ - bool isRefineableTfFun(Node tf); - /** get approximate sqrt * * This approximates the square root of positive constant c. If this method diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index cd9352b3a..af384be49 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -781,7 +781,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; std::vector<Node> pvars; std::vector<Node> psubs; - for (std::pair<const Node, Node>& tb : d_tr_base) + for (std::pair<const Node, Node>& tb : d_trMaster) { pvars.push_back(tb.first); psubs.push_back(tb.second); @@ -804,18 +804,16 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, } // get model bounds for all transcendental functions - Trace("nl-ext-cm-debug") << " get bounds for transcendental functions..." - << std::endl; - for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map) + Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..." + << std::endl; + for (std::pair<const Kind, std::vector<Node> >& tfs : d_funcMap) { Kind k = tfs.first; for (const Node& tf : tfs.second) { + Trace("nl-ext-cm") << "- Term: " << tf << std::endl; bool success = true; // tf is Figure 3 : tf( x ) - Node atf = d_model.computeConcreteModelValue(tf); - Trace("nl-ext-cm-debug") - << "Value for is " << tf << " is " << atf << std::endl; Node bl; Node bu; if (k == PI) @@ -823,41 +821,46 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, bl = d_pi_bound[0]; bu = d_pi_bound[1]; } - else if (d_model.isRefineableTfFun(tf)) + else { - d_model.setUsedApproximate(); std::pair<Node, Node> bounds = getTfModelBounds(tf, d_taylor_degree); bl = bounds.first; bu = bounds.second; + if (bl != bu) + { + d_model.setUsedApproximate(); + } } if (!bl.isNull() && !bu.isNull()) { - // We have rewritten an application of a transcendental function - // based on the current model values.It could be that the model value - // rewrites sin(x) ---> sin(-c) ---> -sin(c), thus we need - // to negate the bounds in this case. - if (atf.getKind() != tf.getKind()) + // for each function in the congruence classe + for (const Node& ctf : d_funcCongClass[tf]) { - if (atf.getKind() == MULT && atf.getNumChildren() == 2 - && atf[0] == d_neg_one) + // each term in congruence classes should be master terms + Assert(d_trSlaves.find(ctf) != d_trSlaves.end()); + // we set the bounds for each slave of tf + for (const Node& stf : d_trSlaves[ctf]) { - atf = atf[1]; - Node btmp = bl; - bl = ArithMSum::negate(bu); - bu = ArithMSum::negate(btmp); + Trace("nl-ext-cm") << "...bound for " << stf << " : [" << bl << ", " + << bu << "]" << std::endl; + success = d_model.addCheckModelBound(stf, bl, bu); } } - success = d_model.addCheckModelBound(atf, bl, bu); + } + else + { + Trace("nl-ext-cm") << "...no bound for " << tf << std::endl; } if (!success) { - Trace("nl-ext-cm-debug") - << "...failed to set bound for transcendental function." - << std::endl; + // a bound was conflicting + Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl; + Trace("nl-ext-cm") << "-----" << std::endl; return false; } } } + Trace("nl-ext-cm") << "-----" << std::endl; bool ret = d_model.checkModel( passertions, false_asserts, d_taylor_degree, lemmas, gs); return ret; @@ -923,7 +926,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, d_ci.clear(); d_ci_exp.clear(); d_ci_max.clear(); - d_f_map.clear(); + d_funcCongClass.clear(); + d_funcMap.clear(); d_tf_region.clear(); std::vector<Node> lemmas; @@ -932,7 +936,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, Trace("nl-ext-mv") << "Extended terms : " << std::endl; // register the extended function terms std::map< Node, Node > mvarg_to_term; - std::vector<Node> tr_no_base; + std::vector<Node> trNeedsMaster; bool needPi = false; // for computing congruence std::map<Kind, ArgTrie> argTrie; @@ -943,6 +947,47 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, d_model.computeAbstractModelValue(a); d_model.printModelValue("nl-ext-mv", a); Kind ak = a.getKind(); + bool consider = true; + // if is an unpurified application of SINE, or it is a transcendental + // applied to a trancendental, purify. + if (isTranscendentalKind(ak)) + { + // if we've already computed master for a + if (d_trMaster.find(a) != d_trMaster.end()) + { + // a master has at least one slave + consider = (d_trSlaves.find(a) != d_trSlaves.end()); + } + else + { + if (ak == SINE) + { + // always not a master + consider = false; + } + else + { + for (const Node& ac : a) + { + if (isTranscendentalKind(ac.getKind())) + { + consider = false; + break; + } + } + } + if (!consider) + { + // wait to assign a master below + trNeedsMaster.push_back(a); + } + else + { + d_trMaster[a] = a; + d_trSlaves[a].push_back(a); + } + } + } if (ak == NONLINEAR_MULT) { d_ms.push_back( a ); @@ -969,31 +1014,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, { needPi = true; } - bool consider = true; - // if is an unpurified application of SINE, or it is a transcendental - // applied to a trancendental, purify. - if (isTranscendentalKind(ak)) - { - if (ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end()) - { - consider = false; - } - else - { - for (const Node& ac : a) - { - if (isTranscendentalKind(ac.getKind())) - { - consider = false; - break; - } - } - } - if (!consider) - { - tr_no_base.push_back(a); - } - } + // if we didn't indicate that it should be purified above if( consider ){ std::vector<Node> repList; for (const Node& ac : a) @@ -1022,14 +1043,19 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } else { - d_f_map[ak].push_back(a); + // new representative of congruence class + d_funcMap[ak].push_back(a); } + // add to congruence class + d_funcCongClass[aa].push_back(a); } } else if (ak == PI) { + Assert(consider); needPi = true; - d_f_map[ak].push_back(a); + d_funcMap[ak].push_back(a); + d_funcCongClass[a].push_back(a); } else { @@ -1052,47 +1078,50 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } // process SINE phase shifting - for (const Node& a : tr_no_base) - { - if (d_tr_base.find(a) == d_tr_base.end()) + for (const Node& a : trNeedsMaster) + { + // should not have processed this already + Assert(d_trMaster.find(a) == d_trMaster.end()); + Kind k = a.getKind(); + Assert(k == SINE || k == EXPONENTIAL); + Node y = + nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg"); + Node new_a = nm->mkNode(k, y); + d_trSlaves[new_a].push_back(new_a); + d_trSlaves[new_a].push_back(a); + d_trMaster[a] = new_a; + d_trMaster[new_a] = new_a; + Node lem; + if (k == SINE) + { + Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a + << std::endl; + Assert(!d_pi.isNull()); + Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts"); + // TODO : do not introduce shift here, instead needs model-based + // refinement for constant shifts (cvc4-projects #1284) + lem = nm->mkNode( + AND, + mkValidPhase(y, d_pi), + nm->mkNode( + ITE, + mkValidPhase(a[0], d_pi), + a[0].eqNode(y), + a[0].eqNode(nm->mkNode( + PLUS, + y, + nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))), + new_a.eqNode(a)); + } + else { - Node y = - nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg"); - Node new_a = nm->mkNode(a.getKind(), y); - d_tr_is_base[new_a] = true; - d_tr_base[a] = new_a; - Node lem; - if (a.getKind() == SINE) - { - Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a - << std::endl; - Assert(!d_pi.isNull()); - Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts"); - // FIXME : do not introduce shift here, instead needs model-based - // refinement for constant shifts (#1284) - lem = nm->mkNode( - AND, - mkValidPhase(y, d_pi), - nm->mkNode( - ITE, - mkValidPhase(a[0], d_pi), - a[0].eqNode(y), - a[0].eqNode(nm->mkNode( - PLUS, - y, - nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))), - new_a.eqNode(a)); - } - else - { - // do both equalities to ensure that new_a becomes a preregistered term - lem = nm->mkNode(AND, a.eqNode(new_a), a[0].eqNode(y)); - } - // must do preprocess on this one - Trace("nl-ext-lemma") - << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - lemsPp.push_back(lem); + // do both equalities to ensure that new_a becomes a preregistered term + lem = nm->mkNode(AND, a.eqNode(new_a), a[0].eqNode(y)); } + // note we must do preprocess on this lemma + Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem + << std::endl; + lemsPp.push_back(lem); } if (!lemsPp.empty()) { @@ -1123,7 +1152,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, { Trace("nl-ext-mv") << "Arguments of trancendental functions : " << std::endl; - for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map) + for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap) { Kind k = tfl.first; if (k == SINE || k == EXPONENTIAL) @@ -2774,7 +2803,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() { std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() { std::vector< Node > lemmas; Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl; - for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map) + for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap) { Kind k = tfl.first; for (const Node& t : tfl.second) @@ -2788,9 +2817,11 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() { Node symn = NodeManager::currentNM()->mkNode( SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0])); symn = Rewriter::rewrite( symn ); - //can assume its basis since phase is split over 0 - d_tr_is_base[symn] = true; - Assert(d_tr_is_base.find(t) != d_tr_is_base.end()); + // Can assume it is its own master since phase is split over 0, + // hence -pi <= t[0] <= pi implies -pi <= -t[0] <= pi. + d_trMaster[symn] = symn; + d_trSlaves[symn].push_back(symn); + Assert(d_trSlaves.find(t) != d_trSlaves.end()); std::vector< Node > children; lem = NodeManager::currentNM()->mkNode( @@ -2884,7 +2915,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { std::map< Kind, std::vector< Node > > sorted_tf_args; std::map< Kind, std::map< Node, Node > > tf_arg_to_term; - for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map) + for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap) { Kind k = tfl.first; if (k == EXPONENTIAL || k == SINE) @@ -2908,7 +2939,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { //sort by concrete values smv.d_isConcrete = true; smv.d_reverse_order = true; - for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map) + for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap) { Kind k = tfl.first; if( !sorted_tf_args[k].empty() ){ @@ -3045,7 +3076,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes( << std::endl; // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions // via Incremental Linearization" by Cimatti et al - for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map) + for (std::pair<const Kind, std::vector<Node> >& tfs : d_funcMap) { Kind k = tfs.first; if (k == PI) @@ -3070,24 +3101,21 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes( for (const Node& tf : tfs.second) { // tf is Figure 3 : tf( x ) - if (d_model.isRefineableTfFun(tf)) + Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl; + // go until max degree is reached, or we don't meet bound criteria + for (unsigned d = 1; d <= d_taylor_degree; d++) { - Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl; - // go until max degree is reached, or we don't meet bound criteria - for (unsigned d = 1; d <= d_taylor_degree; d++) + Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl; + unsigned prev = lemmas.size(); + if (checkTfTangentPlanesFun(tf, d, lemmas, lemSE)) { - Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl; - unsigned prev = lemmas.size(); - if (!checkTfTangentPlanesFun(tf, d, lemmas, lemSE)) - { - Trace("nl-ext-tftp") - << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl; - break; - } - else - { - Trace("nl-ext-tftp") << "...success" << std::endl; - } + Trace("nl-ext-tftp") + << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl; + break; + } + else + { + Trace("nl-ext-tftp") << "...success" << std::endl; } } } @@ -3102,14 +3130,19 @@ bool NonlinearExtension::checkTfTangentPlanesFun( std::vector<Node>& lemmas, std::map<Node, NlLemmaSideEffect>& lemSE) { - Assert(d_model.isRefineableTfFun(tf)); - NodeManager* nm = NodeManager::currentNM(); Kind k = tf.getKind(); + // this should only be run on master applications + Assert(d_trSlaves.find(tf) != d_trSlaves.end()); // Figure 3 : c Node c = d_model.computeAbstractModelValue(tf[0]); int csign = c.getConst<Rational>().sgn(); + if (csign == 0) + { + // no secant/tangent plane is necessary + return true; + } Assert(csign == 1 || csign == -1); // Figure 3: P_l, P_u @@ -3148,7 +3181,8 @@ bool NonlinearExtension::checkTfTangentPlanesFun( Trace("nl-ext-tftp-debug") << " concavity is : " << concavity << std::endl; if (concavity == 0) { - return false; + // no secant/tangent plane is necessary + return true; } // bounds for which we are this concavity // Figure 3: < l, u > @@ -3239,7 +3273,7 @@ bool NonlinearExtension::checkTfTangentPlanesFun( else { // we may want to continue getting better bounds - return true; + return false; } if (is_tangent) @@ -3415,7 +3449,7 @@ bool NonlinearExtension::checkTfTangentPlanesFun( // secant point c for (tf,d). lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c)); } - return false; + return true; } int NonlinearExtension::regionToMonotonicityDir(Kind k, int region) @@ -3819,11 +3853,21 @@ std::pair<Node, Node> NonlinearExtension::getTfModelBounds(Node tf, unsigned d) Node c = d_model.computeAbstractModelValue(tf[0]); Assert(c.isConst()); int csign = c.getConst<Rational>().sgn(); - Assert(csign != 0); + Kind k = tf.getKind(); + if (csign == 0) + { + // at zero, its trivial + if (k == SINE) + { + return std::pair<Node, Node>(d_zero, d_zero); + } + Assert(k == EXPONENTIAL); + return std::pair<Node, Node>(d_one, d_one); + } bool isNeg = csign == -1; std::vector<Node> pbounds; - getPolynomialApproximationBoundForArg(tf.getKind(), c, d, pbounds); + getPolynomialApproximationBoundForArg(k, c, d, pbounds); std::vector<Node> bounds; TNode tfv = d_taylor_real_fv; diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 64a601cc5..2fda9a895 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -511,13 +511,21 @@ class NonlinearExtension { //transcendental functions /** - * Maps arguments of SINE applications to a fresh skolem. This is used for - * ensuring that the argument of SINE we process are on the interval - * [-pi .. pi]. + * Some transcendental functions f(t) are "purified", e.g. we add + * t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not + * purified we call "master terms". + * + * The maps below maintain a master/slave relationship over + * transcendental functions (SINE, EXPONENTIAL, PI), where above + * f(y) is the master of itself and of f(t). + * + * This is used for ensuring that the argument y of SINE we process is on the + * interval [-pi .. pi], and that exponentials are not applied to arguments + * that contain transcendental functions. */ - std::map<Node, Node> d_tr_base; - /** Stores skolems in the range of the above map */ - std::map<Node, bool> d_tr_is_base; + std::map<Node, Node> d_trMaster; + std::map<Node, std::vector<Node> > d_trSlaves; + /** The transcendental functions we have done initial refinements on */ std::map< Node, bool > d_tf_initial_refine; void mkPi(); @@ -544,8 +552,24 @@ class NonlinearExtension { std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp; std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max; - /** A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } */ - std::map<Kind, std::vector<Node> > d_f_map; + /** + * Maps representives of a congruence class to the members of that class. + * + * In detail, a congruence class is a set of terms of the form + * { f(t1), ..., f(tn) } + * such that t1 = ... = tn in the current context. We choose an arbitrary + * term among these to be the repesentative of this congruence class. + * + * Moreover, notice we compute congruence classes only over terms that + * are transcendental function applications that are "master terms", + * see d_trMaster/d_trSlave. + */ + std::map<Node, std::vector<Node> > d_funcCongClass; + /** + * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } + * that are representives of their congruence class. + */ + std::map<Kind, std::vector<Node> > d_funcMap; // factor skolems std::map< Node, Node > d_factor_skolem; @@ -644,13 +668,6 @@ class NonlinearExtension { * on the model value of its argument. */ std::pair<Node, Node> getTfModelBounds(Node tf, unsigned d); - /** is refinable transcendental function - * - * A transcendental function application is not refineable if its current - * model value is zero, or if it is an application of SINE applied - * to a non-variable. - */ - bool isRefineableTfFun(Node tf); /** get approximate sqrt * * This approximates the square root of positive constant c. If this method @@ -953,14 +970,20 @@ class NonlinearExtension { std::map<Node, NlLemmaSideEffect>& lemSE); /** check transcendental function refinement for tf * - * This method is called by the above method for each refineable - * transcendental function (see isRefineableTfFun) that occurs in an - * assertion in the current context. + * This method is called by the above method for each "master" + * transcendental function application that occurs in an assertion in the + * current context. For example, an application like sin(t) is not a master + * if we have introduced the constraints: + * t=y+2*pi*n ^ -pi <= y <= pi ^ sin(t) = sin(y). + * See d_trMaster/d_trSlaves for more detail. * * This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental * function application tf for Taylor degree d. It may add a secant or * tangent plane lemma to lems and its side effect (if one exists) * to lemSE. + * + * It returns false if the bounds are not precise enough to add a + * secant or tangent plane lemma. */ bool checkTfTangentPlanesFun(Node tf, unsigned d, diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 5414c9b98..e2cafa4d3 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,10 +16,10 @@ #include "theory/strings/core_solver.h" -#include "theory/strings/theory_strings_utils.h" #include "options/strings_options.h" #include "theory/strings/theory_strings_rewriter.h" - +#include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" using namespace std; using namespace CVC4::context; @@ -37,7 +37,7 @@ d_nf_pairs(c) d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + d_emptyString = Word::mkEmptyWord(CONST_STRING); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); } @@ -1071,10 +1071,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Assert(!d_state.areEqual(x, y)); std::vector<Node> lenExp; - Node xLen = d_state.getLength(x, lenExp); - Node yLen = d_state.getLength(y, lenExp); + Node xLenTerm = d_state.getLength(x, lenExp); + Node yLenTerm = d_state.getLength(y, lenExp); - if (d_state.areEqual(xLen, yLen)) + if (d_state.areEqual(xLenTerm, yLenTerm)) { // `x` and `y` have the same length. We infer that the two components // have to be the same. @@ -1083,7 +1083,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl; Node eq = x.eqNode(y); - Node leneq = xLen.eqNode(yLen); + Node leneq = xLenTerm.eqNode(yLenTerm); NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, lenExp); lenExp.push_back(leneq); d_im.sendInference(lenExp, eq, "N_Unify"); @@ -1137,13 +1137,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // Constants in both normal forms. // // E.g. "abc" ++ ... = "ab" ++ ... - String c1 = x.getConst<String>(); - String c2 = y.getConst<String>(); + size_t lenX = Word::getLength(x); + size_t lenY = Word::getLength(y); Trace("strings-solve-debug") << "Simple Case 4 : Const Split : " << x << " vs " << y << " at index " << index << ", isRev = " << isRev << std::endl; - size_t minLen = std::min(c1.size(), c2.size()); - bool isSameFix = isRev ? c1.rstrncmp(c2, minLen) : c1.strncmp(c2, minLen); + size_t minLen = std::min(lenX, lenY); + bool isSameFix = + isRev ? Word::rstrncmp(x, y, minLen) : Word::strncmp(x, y, minLen); if (isSameFix) { // The shorter constant is a prefix/suffix of the longer constant. We @@ -1152,20 +1153,20 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // // E.g. "abc" ++ x' ++ ... = "ab" ++ y' ++ ... ---> // "c" ++ x' ++ ... = y' ++ ... - bool c1Shorter = c1.size() < c2.size(); - NormalForm& nfl = c1Shorter ? nfj : nfi; - const String& cl = c1Shorter ? c2 : c1; - Node ns = c1Shorter ? x : y; + bool xShorter = lenX < lenY; + NormalForm& nfl = xShorter ? nfj : nfi; + Node cl = xShorter ? y : x; + Node ns = xShorter ? x : y; Node remainderStr; if (isRev) { - int newlen = cl.size() - minLen; - remainderStr = nm->mkConst(cl.substr(0, newlen)); + size_t newlen = std::max(lenX, lenY) - minLen; + remainderStr = Word::substr(cl, 0, newlen); } else { - remainderStr = nm->mkConst(cl.substr(minLen)); + remainderStr = Word::substr(cl, minLen); } Trace("strings-solve-debug-test") << "Break normal form of " << cl << " into " << ns << ", " @@ -1195,7 +1196,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, info.d_j = nfj.d_base; info.d_rev = isRev; Assert(index < nfiv.size() - rproc && index < nfjv.size() - rproc); - if (!d_state.areDisequal(xLen, yLen) && !d_state.areEqual(xLen, yLen) + if (!d_state.areDisequal(xLenTerm, yLenTerm) && !d_state.areEqual(xLenTerm, yLenTerm) && !x.isConst() && !y.isConst()) // AJR: remove the latter 2 conditions? { @@ -1207,7 +1208,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl; - Node lenEq = nm->mkNode(EQUAL, xLen, yLen); + Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm); lenEq = Rewriter::rewrite(lenEq); info.d_conc = nm->mkNode(OR, lenEq, lenEq.negate()); info.d_pending_phase[lenEq] = true; @@ -1395,7 +1396,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // is a prefix/suffix of the other. // // E.g. x ++ ... = y ++ ... ---> (x = y ++ k) v (y = x ++ k) - Assert(d_state.areDisequal(xLen, yLen)); + Assert(d_state.areDisequal(xLenTerm, yLenTerm)); Assert(x.getKind() != CONST_STRING); Assert(y.getKind() != CONST_STRING); @@ -1411,8 +1412,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // do not infer constants are larger than variables if (t.getKind() != CONST_STRING) { - Node lt1 = e == 0 ? xLen : yLen; - Node lt2 = e == 0 ? yLen : xLen; + Node lt1 = e == 0 ? xLenTerm : yLenTerm; + Node lt2 = e == 0 ? yLenTerm : xLenTerm; Node entLit = Rewriter::rewrite(nm->mkNode(GT, lt1, lt2)); std::pair<bool, Node> et = d_state.entailmentCheck( options::TheoryOfMode::THEORY_OF_TYPE_BASED, entLit); @@ -1465,7 +1466,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, } else { - Node ldeq = nm->mkNode(EQUAL, xLen, yLen).negate(); + Node ldeq = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate(); info.d_ant.push_back(ldeq); info.d_conc = nm->mkNode(OR, eq1, eq2); info.d_id = INFER_SSPLIT_VAR; @@ -1625,13 +1626,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, { Trace("strings-loop") << "Strings::Loop: Const Normal Breaking." << std::endl; - CVC4::String s = t_yz.getConst<CVC4::String>(); - unsigned size = s.size(); + unsigned size = Word::getLength(t_yz); std::vector<Node> vconc; for (unsigned len = 1; len <= size; len++) { - Node y = nm->mkConst(s.substr(0, len)); - Node z = nm->mkConst(s.substr(len, size - len)); + Node y = Word::substr(t_yz, 0, len); + Node z = Word::substr(t_yz, len, size - len); Node restr = s_zy; Node cc; if (r != d_emptyString) @@ -1770,8 +1770,9 @@ void CoreSolver::processDeq( Node ni, Node nj ) { return; }else{ //split on first character - CVC4::String str = const_k.getConst<String>(); - Node firstChar = str.size() == 1 ? const_k : NodeManager::currentNM()->mkConst( str.prefix( 1 ) ); + Node firstChar = Word::getLength(const_k) == 1 + ? const_k + : Word::prefix(const_k, 1); if (d_state.areEqual(lnck, d_one)) { if (d_state.areDisequal(firstChar, nconst_k)) @@ -1947,26 +1948,31 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& if (!d_state.areEqual(i, j)) { if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) { - unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size(); + size_t lenI = Word::getLength(i); + size_t lenJ = Word::getLength(j); + unsigned int len_short = lenI < lenJ ? lenI : lenJ; bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short); if( isSameFix ) { //same prefix/suffix //k is the index of the string that is shorter - Node nk = i.getConst<String>().size() < j.getConst<String>().size() ? i : j; - Node nl = i.getConst<String>().size() < j.getConst<String>().size() ? j : i; + Node nk = lenI < lenJ ? i : j; + Node nl = lenI < lenJ ? j : i; Node remainderStr; if( isRev ){ - int new_len = nl.getConst<String>().size() - len_short; - remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr(0, new_len) ); + int new_len = Word::getLength(nl) - len_short; + remainderStr = Word::substr(nl, 0, new_len); Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl; } else { - remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr( len_short ) ); + remainderStr = Word::substr(nl, len_short); Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl; } - if( i.getConst<String>().size() < j.getConst<String>().size() ) { + if (lenI < lenJ) + { nfj.insert( nfj.begin() + index + 1, remainderStr ); nfj[index] = nfi[index]; - } else { + } + else + { nfi.insert( nfi.begin() + index + 1, remainderStr ); nfi[index] = nfj[index]; } diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 530564a35..f91b59834 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -20,6 +20,7 @@ #include "options/strings_options.h" #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" using namespace CVC4; using namespace CVC4::kind; @@ -29,11 +30,8 @@ namespace theory { namespace strings { RegExpOpr::RegExpOpr() - : d_emptyString(NodeManager::currentNM()->mkConst(::CVC4::String(""))), - d_true(NodeManager::currentNM()->mkConst(true)), + : d_true(NodeManager::currentNM()->mkConst(true)), d_false(NodeManager::currentNM()->mkConst(false)), - d_emptySingleton(NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, - d_emptyString)), d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY, std::vector<Node>{})), d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))), @@ -42,6 +40,10 @@ RegExpOpr::RegExpOpr() std::vector<Node>{})), d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma)) { + d_emptyString = Word::mkEmptyWord(CONST_STRING); + + d_emptySingleton = + NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, d_emptyString); d_lastchar = utils::getAlphabetCardinality() - 1; } @@ -295,6 +297,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { int ret = 1; retNode = d_emptyRegexp; + NodeManager* nm = NodeManager::currentNM(); PairNodeStr dv = std::make_pair( r, c ); if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) { @@ -332,10 +335,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { if(tmp == d_emptyString) { ret = 2; } else { - if (tmp.getConst<CVC4::String>().front() == c.front()) + if (tmp.getConst<String>().front() == c.front()) { - retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, - tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) ); + retNode = + nm->mkNode(STRING_TO_REGEXP, + Word::getLength(tmp) == 1 ? d_emptyString + : Word::substr(tmp, 1)); } else { ret = 2; } @@ -346,10 +351,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { if(tmp.getKind() == kind::STRING_CONCAT) { Node t2 = tmp[0]; if(t2.isConst()) { - if (t2.getConst<CVC4::String>().front() == c.front()) + if (t2.getConst<String>().front() == c.front()) { - Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, - tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) ); + Node n = nm->mkNode(STRING_TO_REGEXP, + Word::getLength(tmp) == 1 + ? d_emptyString + : Word::substr(tmp, 1)); std::vector< Node > vec_nodes; vec_nodes.push_back(n); for(unsigned i=1; i<tmp.getNumChildren(); i++) { @@ -541,6 +548,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { Trace("regexp-derive") << "RegExp-derive starts with /" << mkString( r ) << "/, c=" << c << std::endl; Node retNode = d_emptyRegexp; PairNodeStr dv = std::make_pair( r, c ); + NodeManager* nm = NodeManager::currentNM(); if( d_dv_cache.find( dv ) != d_dv_cache.end() ) { retNode = d_dv_cache[dv]; } else if( c.isEmptyString() ){ @@ -576,10 +584,12 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { if(r[0] == d_emptyString) { retNode = d_emptyRegexp; } else { - if (r[0].getConst<CVC4::String>().front() == c.front()) + if (r[0].getConst<String>().front() == c.front()) { - retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, - r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) ); + retNode = nm->mkNode(STRING_TO_REGEXP, + Word::getLength(r[0]) == 1 + ? d_emptyString + : Word::substr(r[0], 1)); } else { retNode = d_emptyRegexp; } @@ -743,7 +753,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) case kind::STRING_TO_REGEXP: { Node st = Rewriter::rewrite(r[0]); if(st.isConst()) { - CVC4::String s = st.getConst< CVC4::String >(); + String s = st.getConst<String>(); if(s.size() != 0) { unsigned sc = s.front(); sc = String::convertUnsignedIntToCode(sc); @@ -753,7 +763,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) else if (st.getKind() == kind::STRING_CONCAT) { if(st[0].isConst()) { - CVC4::String s = st[0].getConst<CVC4::String>(); + String s = st[0].getConst<String>(); unsigned sc = s.front(); sc = String::convertUnsignedIntToCode(sc); cset.insert(sc); @@ -1638,7 +1648,7 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) { //printing std::string RegExpOpr::niceChar(Node r) { if(r.isConst()) { - std::string s = r.getConst<CVC4::String>().toString() ; + std::string s = r.getConst<String>().toString(); return s == "." ? "\\." : s; } else { std::string ss = "$" + r.toString(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a5604925c..5015db3f1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -29,6 +29,7 @@ #include "theory/strings/theory_strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/type_enumerator.h" +#include "theory/strings/word.h" #include "theory/theory_model.h" #include "theory/valuation.h" @@ -111,7 +112,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + d_emptyString = Word::mkEmptyWord(CONST_STRING); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index a0ee0d224..dd573b68c 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -78,6 +78,34 @@ size_t Word::getLength(TNode x) bool Word::isEmpty(TNode x) { return getLength(x) == 0; } +bool Word::strncmp(TNode x, TNode y, std::size_t n) +{ + Kind k = x.getKind(); + if (k == CONST_STRING) + { + Assert(y.getKind() == CONST_STRING); + String sx = x.getConst<String>(); + String sy = y.getConst<String>(); + return sx.strncmp(sy, n); + } + Unimplemented(); + return false; +} + +bool Word::rstrncmp(TNode x, TNode y, std::size_t n) +{ + Kind k = x.getKind(); + if (k == CONST_STRING) + { + Assert(y.getKind() == CONST_STRING); + String sx = x.getConst<String>(); + String sy = y.getConst<String>(); + return sx.rstrncmp(sy, n); + } + Unimplemented(); + return false; +} + std::size_t Word::find(TNode x, TNode y, std::size_t start) { Kind k = x.getKind(); diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index 74f50ee9a..7b813a0b2 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -45,6 +45,22 @@ class Word /** Return true if x is empty */ static bool isEmpty(TNode x); + /** string compare + * + * Returns true if x is equal to y for their first n characters. + * If n is larger than the length of x or y, this method returns + * true if and only if x is equal to y. + */ + static bool strncmp(TNode x, TNode y, std::size_t n); + + /** reverse string compare + * + * Returns true if x is equal to y for their last n characters. + * If n is larger than the length of tx or y, this method returns + * true if and only if x is equal to y. + */ + static bool rstrncmp(TNode x, TNode y, std::size_t n); + /** Return the first position y occurs in x, or std::string::npos otherwise */ static std::size_t find(TNode x, TNode y, std::size_t start = 0); diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 4dfe68b51..00066edb6 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -88,8 +88,8 @@ String String::concat(const String &other) const { return String(ret_vec); } -bool String::strncmp(const String &y, const std::size_t np) const { - std::size_t n = np; +bool String::strncmp(const String& y, std::size_t n) const +{ std::size_t b = (size() >= y.size()) ? size() : y.size(); std::size_t s = (size() <= y.size()) ? size() : y.size(); if (n > s) { @@ -105,8 +105,8 @@ bool String::strncmp(const String &y, const std::size_t np) const { return true; } -bool String::rstrncmp(const String &y, const std::size_t np) const { - std::size_t n = np; +bool String::rstrncmp(const String& y, std::size_t n) const +{ std::size_t b = (size() >= y.size()) ? size() : y.size(); std::size_t s = (size() <= y.size()) ? size() : y.size(); if (n > s) { diff --git a/src/util/regexp.h b/src/util/regexp.h index 1cde53687..731736f72 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -109,8 +109,18 @@ class CVC4_PUBLIC String { bool operator<=(const String& y) const { return cmp(y) <= 0; } bool operator>=(const String& y) const { return cmp(y) >= 0; } - bool strncmp(const String& y, const std::size_t np) const; - bool rstrncmp(const String& y, const std::size_t np) const; + /** + * Returns true if this string is equal to y for their first n characters. + * If n is larger than the length of this string or y, this method returns + * true if and only if this string is equal to y. + */ + bool strncmp(const String& y, std::size_t n) const; + /** + * Returns true if this string is equal to y for their last n characters. + * Similar to strncmp, if n is larger than the length of this string or y, + * this method returns true if and only if this string is equal to y. + */ + bool rstrncmp(const String& y, std::size_t n) const; /* toString * Converts this string to a std::string. |