From 2b4d6997eec82dce3832a449eea00f94af420f8a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 22 Nov 2020 19:41:23 -0600 Subject: Fix quantifiers scope issue in strings preprocessor (#5491) Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL. Fixes #5483. --- src/theory/strings/theory_strings_preprocess.cpp | 4 +++- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/issue5483-pp-leq.smt2 | 9 +++++++++ 3 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/strings/issue5483-pp-leq.smt2 diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 81ec79327..87ab533f4 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -965,7 +965,9 @@ Node StringsPreprocess::simplifyRec(Node t, Node retNode = t; if( t.getNumChildren()==0 ){ retNode = simplify(t, asserts); - }else if( t.getKind()!=kind::FORALL ){ + } + else if (!t.isClosure()) + { bool changed = false; std::vector< Node > cc; if( t.getMetaKind() == kind::metakind::PARAMETERIZED ){ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index af238db18..1bf6c63f0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1862,6 +1862,7 @@ set(regress_1_tests regress1/strings/issue5330.smt2 regress1/strings/issue5330_2.smt2 regress1/strings/issue5374-proxy-i.smt2 + regress1/strings/issue5483-pp-leq.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue5483-pp-leq.smt2 b/test/regress/regress1/strings/issue5483-pp-leq.smt2 new file mode 100644 index 000000000..9e9900b21 --- /dev/null +++ b/test/regress/regress1/strings/issue5483-pp-leq.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -i +; EXPECT: sat +(set-logic QF_SLIA) +(declare-fun _substvar_21_ () String) +(declare-fun _substvar_29_ () String) +(set-option :strings-lazy-pp false) +(assert (xor true true true true (str.<= _substvar_21_ _substvar_29_) true true)) +(push 1) +(check-sat) -- cgit v1.2.3 From 961af5e182f65c976424fd2adc22fc9bd484f73c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 23 Nov 2020 08:55:03 +0100 Subject: Add get-info :time. (#5485) This PR adds the new info `:time` that can be queried with `(get-info :time)` and returns the spent CPU time (as returned by `std::clock()`. @pjljvandelaar Fixes CVC4/CVC4-projects#102 --- src/smt/smt_engine.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2a0cde015..1d623fdef 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -506,7 +506,7 @@ bool SmtEngine::isValidGetInfoFlag(const std::string& key) const if (key == "all-statistics" || key == "error-behavior" || key == "name" || key == "version" || key == "authors" || key == "status" || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options") + || key == "all-options" || key == "time") { return true; } @@ -578,6 +578,10 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const default: return SExpr(SExpr::Keyword("unknown")); } } + if (key == "time") + { + return SExpr(std::clock()); + } if (key == "reason-unknown") { Result status = d_state->getStatus(); -- cgit v1.2.3 From e11af4be0f3d1dee41aefa91d856de9035cb3a29 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 06:40:47 -0600 Subject: Add declare model symbol methods to SymbolManager and Model (#5480) This is in preparation for the symbol manager determining which symbols are printed in the model. --- src/expr/symbol_manager.cpp | 63 +++++++++++++++++++++++++++++++++++++++++++++ src/expr/symbol_manager.h | 17 ++++++++++++ src/smt/model.cpp | 14 ++++++++++ src/smt/model.h | 39 +++++++++++++++++++++++++--- 4 files changed, 129 insertions(+), 4 deletions(-) diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index a163e503d..f82845fe3 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -16,6 +16,7 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" +#include "context/cdlist.h" #include "context/cdo.h" using namespace CVC4::context; @@ -28,12 +29,16 @@ class SymbolManager::Implementation { using TermStringMap = CDHashMap; using TermSet = CDHashSet; + using SortList = CDList; + using TermList = CDList; public: Implementation() : d_context(), d_names(&d_context), d_namedAsserts(&d_context), + d_declareSorts(&d_context), + d_declareTerms(&d_context), d_hasPushedScope(&d_context, false) { } @@ -53,6 +58,14 @@ class SymbolManager::Implementation bool areAssertions = false) const; /** get expression names */ std::map getExpressionNames(bool areAssertions) const; + /** get model declare sorts */ + std::vector getModelDeclareSorts() const; + /** get model declare terms */ + std::vector getModelDeclareTerms() const; + /** Add declared sort to the list of model declarations. */ + void addModelDeclarationSort(api::Sort s); + /** Add declared term to the list of model declarations. */ + void addModelDeclarationTerm(api::Term t); /** reset */ void reset(); /** Push a scope in the expression names. */ @@ -67,6 +80,10 @@ class SymbolManager::Implementation TermStringMap d_names; /** The set of terms with assertion names */ TermSet d_namedAsserts; + /** Declared sorts (for model printing) */ + SortList d_declareSorts; + /** Declared terms (for model printing) */ + TermList d_declareTerms; /** * Have we pushed a scope (e.g. a let or quantifier) in the current context? */ @@ -150,6 +167,34 @@ SymbolManager::Implementation::getExpressionNames(bool areAssertions) const return emap; } +std::vector SymbolManager::Implementation::getModelDeclareSorts() + const +{ + std::vector declareSorts(d_declareSorts.begin(), + d_declareSorts.end()); + return declareSorts; +} + +std::vector SymbolManager::Implementation::getModelDeclareTerms() + const +{ + std::vector declareTerms(d_declareTerms.begin(), + d_declareTerms.end()); + return declareTerms; +} + +void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s) +{ + Trace("sym-manager") << "addModelDeclarationSort " << s << std::endl; + d_declareSorts.push_back(s); +} + +void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t) +{ + Trace("sym-manager") << "addModelDeclarationTerm " << t << std::endl; + d_declareTerms.push_back(t); +} + void SymbolManager::Implementation::pushScope(bool isUserContext) { Trace("sym-manager") << "pushScope, isUserContext = " << isUserContext @@ -219,6 +264,24 @@ std::map SymbolManager::getExpressionNames( { return d_implementation->getExpressionNames(areAssertions); } +std::vector SymbolManager::getModelDeclareSorts() const +{ + return d_implementation->getModelDeclareSorts(); +} +std::vector SymbolManager::getModelDeclareTerms() const +{ + return d_implementation->getModelDeclareTerms(); +} + +void SymbolManager::addModelDeclarationSort(api::Sort s) +{ + d_implementation->addModelDeclarationSort(s); +} + +void SymbolManager::addModelDeclarationTerm(api::Term t) +{ + d_implementation->addModelDeclarationTerm(t); +} size_t SymbolManager::scopeLevel() const { diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index a3ca8e780..06b01da8b 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -92,6 +92,23 @@ class CVC4_PUBLIC SymbolManager */ std::map getExpressionNames( bool areAssertions = false) const; + /** + * @return The sorts we have declared that should be printed in the model. + */ + std::vector getModelDeclareSorts() const; + /** + * @return The terms we have declared that should be printed in the model. + */ + std::vector getModelDeclareTerms() const; + /** + * Add declared sort to the list of model declarations. + */ + void addModelDeclarationSort(api::Sort s); + /** + * Add declared term to the list of model declarations. + */ + void addModelDeclarationTerm(api::Term t); + //---------------------------- end named expressions /** * Get the scope level of the symbol table. diff --git a/src/smt/model.cpp b/src/smt/model.cpp index fc9ea8fbb..b734ad9e9 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -61,5 +61,19 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } +void Model::clearModelDeclarations() { d_declareSorts.clear(); } + +void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); } + +void Model::addDeclarationTerm(Node n) { d_declareTerms.push_back(n); } +const std::vector& Model::getDeclaredSorts() const +{ + return d_declareSorts; +} +const std::vector& Model::getDeclaredTerms() const +{ + return d_declareTerms; +} + } // namespace smt }/* CVC4 namespace */ diff --git a/src/smt/model.h b/src/smt/model.h index dc36b5d29..0913922d1 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -39,6 +39,9 @@ std::ostream& operator<<(std::ostream&, const Model&); * This is the SMT-level model object, that is responsible for maintaining * the necessary information for how to print the model, as well as * holding a pointer to the underlying implementation of the theory model. + * + * The model declarations maintained by this class are context-independent + * and should be updated when this model is printed. */ class Model { friend std::ostream& operator<<(std::ostream&, const Model&); @@ -49,10 +52,6 @@ class Model { Model(SmtEngine& smt, theory::TheoryModel* tm); /** virtual destructor */ ~Model() {} - /** get number of commands to report */ - size_t getNumCommands() const; - /** get command */ - const NodeCommand* getCommand(size_t i) const; /** get the smt engine that this model is hooked up to */ SmtEngine* getSmtEngine() { return &d_smt; } /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ @@ -78,6 +77,28 @@ class Model { /** Does this model have approximations? */ bool hasApproximations() const; //----------------------- end helper methods + /** get number of commands to report */ + size_t getNumCommands() const; + /** get command */ + const NodeCommand* getCommand(size_t i) const; + //----------------------- model declarations + /** Clear the current model declarations. */ + void clearModelDeclarations(); + /** + * Set that tn is a sort that should be printed in the model, when applicable, + * based on the output language. + */ + void addDeclarationSort(TypeNode tn); + /** + * Set that n is a variable that should be printed in the model, when + * applicable, based on the output language. + */ + void addDeclarationTerm(Node n); + /** get declared sorts */ + const std::vector& getDeclaredSorts() const; + /** get declared terms */ + const std::vector& getDeclaredTerms() const; + //----------------------- end model declarations protected: /** The SmtEngine we're associated with */ SmtEngine& d_smt; @@ -93,6 +114,16 @@ class Model { * the values of sorts and terms. */ theory::TheoryModel* d_tmodel; + /** + * The list of types to print, generally corresponding to declare-sort + * commands. + */ + std::vector d_declareSorts; + /** + * The list of terms to print, is typically one-to-one with declare-fun + * commands. + */ + std::vector d_declareTerms; }; } // namespace smt -- cgit v1.2.3 From 5aa585b74682a7e92a188548ce582eeb1212e42b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 10:23:00 -0600 Subject: (proof-new) Miscellaneous changes from proof-new (#5445) --- src/expr/term_conversion_proof_generator.cpp | 4 +++- src/expr/type_node.cpp | 4 +--- src/smt/preprocessor.cpp | 1 + 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 02613345f..858ca9f64 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -138,7 +138,9 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx) // should not rewrite term to two different things if (!getRewriteStepInternal(thash).isNull()) { - Assert(getRewriteStepInternal(thash) == s); + Assert(getRewriteStepInternal(thash) == s) + << identify() << " rewriting " << t << " to both " << s << " and " + << getRewriteStepInternal(thash); return Node::null(); } d_rewriteMap[thash] = s; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 0818ca8c1..49fbe73ef 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -589,13 +589,11 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { case kind::SEQUENCE_TYPE: case kind::SET_TYPE: case kind::BAG_TYPE: + case kind::SEXPR_TYPE: { // we don't support subtyping except for built in types Int and Real. return TypeNode(); // return null type } - case kind::SEXPR_TYPE: - Unimplemented() - << "haven't implemented leastCommonType for symbolic expressions yet"; default: Unimplemented() << "don't have a commonType for types `" << t0 << "' and `" << t1 << "'"; diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 98a2a7a36..5a1ce63a4 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -158,6 +158,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) { Assert(pppg != nullptr); d_pnm = pppg->getManager(); + d_propagator.setProof(d_pnm, d_context, pppg); d_rtf.setProofNodeManager(d_pnm); } -- cgit v1.2.3 From 2a5a65feac6ce270732f0a4d672e5838f5cd673a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 10:34:53 -0600 Subject: Fix for sygusToBuiltinEval for non-ground composite terms (#5466) There was a bug in the method for computing the evaluation of a sygus term applied to arguments. The case that was wrong was for (DT_SYGUS_EVAL t c1 ... cn) where t contained a subterm (op t1 ... tn) where: (1) (op t1 ... tn) is a non-ground sygus datatype term (2) op was an operator of the form (lambda ((z T)) (g z xi)) where xi is a variable from the formal argument list of the function to synthesize. In this case, xi was not getting replaced by ci. This bug appears when using sygus repair for grammars with composite term that involve variables from the formal argument list of the synth-fun. --- src/theory/datatypes/sygus_datatype_utils.cpp | 19 ++++++++++++++----- src/theory/datatypes/sygus_datatype_utils.h | 20 ++++++++++---------- src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 3 +++ src/theory/quantifiers/sygus/sygus_repair_const.cpp | 4 ++++ 4 files changed, 31 insertions(+), 15 deletions(-) diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 612722d48..f99f58969 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -37,12 +37,19 @@ Node applySygusArgs(const DType& dt, Node n, const std::vector& args) { + // optimization: if n is just a sygus bound variable, return immediately + // by replacing with the proper argument, or returning unchanged if it is + // a bound variable not corresponding to a formal argument. if (n.getKind() == BOUND_VARIABLE) { - Assert(n.hasAttribute(SygusVarNumAttribute())); - int vn = n.getAttribute(SygusVarNumAttribute()); - Assert(dt.getSygusVarList()[vn] == n); - return args[vn]; + if (n.hasAttribute(SygusVarNumAttribute())) + { + int vn = n.getAttribute(SygusVarNumAttribute()); + Assert(dt.getSygusVarList()[vn] == n); + return args[vn]; + } + // it is a different bound variable, it is unchanged + return n; } // n is an application of operator op. // We must compute the free variables in op to determine if there are @@ -551,8 +558,10 @@ Node sygusToBuiltinEval(Node n, const std::vector& args) children.push_back(it->second); } index = indexOf(cur.getOperator()); - // apply to arguments + // apply to children, which constructs the builtin term ret = mkSygusTerm(dt, index, children); + // now apply it to arguments in args + ret = applySygusArgs(dt, dt[index].getSygusOp(), ret, args); } visited[cur] = ret; } diff --git a/src/theory/datatypes/sygus_datatype_utils.h b/src/theory/datatypes/sygus_datatype_utils.h index 3f833702c..fabb295eb 100644 --- a/src/theory/datatypes/sygus_datatype_utils.h +++ b/src/theory/datatypes/sygus_datatype_utils.h @@ -113,7 +113,7 @@ Node mkSygusTerm(Node op, const std::vector& children, bool doBetaReduction = true); /** - * n is a builtin term that is an application of operator op. + * n is a builtin term that is a (rewritten) 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. @@ -122,18 +122,18 @@ Node mkSygusTerm(Node op, * 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 + * C1 / L1 where L1 is (lambda w1 w2. w1+w2) + * C2 / L2 where L2 is (lambda w1. w1+x) + * C3 / L3 where L3 is (lambda w1. w1+(x+y)) + * C4 / L4 where L4 is y * Examples of calling this function: - * applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } ) + * applySygusArgs( dt, L1, (APPLY_UF L1 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 } ) + * applySygusArgs( dt, L2, (APPLY_UF L2 t1), { 3, 5 } ) * ... returns (APPLY_UF (lambda w1. w1+3) t1). - * applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } ) + * applySygusArgs( dt, L3, (APPLY_UF L3 t1), { 3, 5 } ) * ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1). - * applySygusArgs( dt, C4, y, { 3, 5 } ) + * applySygusArgs( dt, L4, L4, { 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 @@ -185,7 +185,7 @@ Node builtinVarToSygus(Node v); * where n' is a variable, then this method returns: * 12 + (DT_SYGUS_EVAL n' 3 4) * Notice that the subterm C_*( C_x(), C_y() ) is converted to its builtin - * equivalent x*y and evaluated under the substition { x -> 3, x -> 4 } giving + * equivalent x*y and evaluated under the substition { x -> 3, y -> 4 } giving * 12. The subterm n' is non-constant and thus we return its evaluation under * 3,4, giving the term (DT_SYGUS_EVAL n' 3 4). Since the top-level constructor * is C_+, these terms are added together to give the result. diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 9f3ed4f4f..882c9ca77 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -314,8 +314,11 @@ Node SygusEvalUnfold::unfold(Node en, Node ret = d_tds->mkGeneric(dt, i, pre); // apply the appropriate substitution to ret ret = datatypes::utils::applySygusArgs(dt, sop, ret, args); + Trace("sygus-eval-unfold-debug") + << "Applied sygus args : " << ret << std::endl; // rewrite ret = Rewriter::rewrite(ret); + Trace("sygus-eval-unfold-debug") << "Rewritten : " << ret << std::endl; return ret; } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 989f7b758..81120da28 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "api/cvc4cpp.h" +#include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -200,7 +201,10 @@ bool SygusRepairConst::repairSolution(Node sygusBody, candidate_skeletons, sk_vars, sk_vars_to_subs); + Trace("sygus-repair-const-debug") + << "...after fit-to-logic : " << fo_body << std::endl; } + Assert(!expr::hasFreeVar(fo_body)); if (fo_body.isNull() || sk_vars.empty()) { -- cgit v1.2.3 From a6c001e078767a2de6f36a2fa1333b98e39a6ec8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 11:49:59 -0600 Subject: Change UF ho to ppRewrite instead of expand definition (#5499) UF uses expandDefinitions to convert fully applied HO_APPLY to APPLY_UF. The more appropriate place to do this is in Theory::ppRewrite. --- src/theory/uf/ho_extension.cpp | 4 ++-- src/theory/uf/ho_extension.h | 4 ++-- src/theory/uf/theory_uf.cpp | 12 ++++++------ src/theory/uf/theory_uf.h | 2 +- test/regress/regress1/ho/NUM925^1.p | 2 +- test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 | 2 +- test/regress/regress2/ho/involved_parsing_ALG248^3.p | 2 +- 7 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index d7de0a025..66bcbc76f 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -36,14 +36,14 @@ HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im) d_true = NodeManager::currentNM()->mkConst(true); } -Node HoExtension::expandDefinition(Node node) +Node HoExtension::ppRewrite(Node node) { // convert HO_APPLY to APPLY_UF if fully applied if (node[0].getType().getNumChildren() == 2) { Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; Node ret = getApplyUfForHoApply(node); - Trace("uf-ho") << "uf-ho : expandDefinition : " << node << " to " << ret + Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret << std::endl; return ret; } diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index fa9c5c612..0e82dbda6 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -54,7 +54,7 @@ class HoExtension public: HoExtension(TheoryState& state, TheoryInferenceManager& im); - /** expand definition + /** ppRewrite * * This returns the expanded form of node. * @@ -63,7 +63,7 @@ class HoExtension * function variables for function heads that are not variables via the * getApplyUfForHoApply method below. */ - Node expandDefinition(Node node); + Node ppRewrite(Node node); /** check higher order * diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 099b56a33..6fdc969a4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -204,21 +204,21 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) } //--------------------------------- end standard check -TrustNode TheoryUF::expandDefinition(Node node) +TrustNode TheoryUF::ppRewrite(TNode node) { - Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : " - << node << std::endl; + Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node + << std::endl; if( node.getKind()==kind::HO_APPLY ){ if( !options::ufHo() ){ std::stringstream ss; ss << "Partial function applications are not supported in default mode, try --uf-ho."; throw LogicException(ss.str()); } - Node ret = d_ho->expandDefinition(node); + Node ret = d_ho->ppRewrite(node); if (ret != node) { - Trace("uf-exp-def") << "TheoryUF::expandDefinition: higher-order: " - << node << " to " << ret << std::endl; + Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node + << " to " << ret << std::endl; return TrustNode::mkTrustRewrite(node, ret, nullptr); } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4a63d9584..3f76919eb 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -142,7 +142,7 @@ private: bool collectModelValues(TheoryModel* m, const std::set& termSet) override; - TrustNode expandDefinition(Node node) override; + TrustNode ppRewrite(TNode node) override; void preRegisterTerm(TNode term) override; TrustNode explain(TNode n) override; diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p index d2977ddb8..e162a63a4 100644 --- a/test/regress/regress1/ho/NUM925^1.p +++ b/test/regress/regress1/ho/NUM925^1.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho +% COMMAND-LINE: --uf-ho --ho-elim % EXPECT: % SZS status Theorem for NUM925^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 index edb55d756..313ff68a1 100644 --- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models +; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim ; EXPECT: unsat (set-logic ALL) diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p index 5ad693629..d0577dd1f 100644 --- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p +++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho +% COMMAND-LINE: --uf-ho --ho-elim % EXPECT: % SZS status Theorem for involved_parsing_ALG248^3 %------------------------------------------------------------------------------ -- cgit v1.2.3 From 07c7b873c5c2ee81cb2672428ca1de0d75bb1ae8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 16:09:20 -0600 Subject: Fix regular expression consume for nested star (#5518) The issue was caused by simple regular expression consume being too aggressive when a recursive call was made to the method. In particular, we were assuming that the body of the star must be unrolled to fully consume a string, when it can be skipped if we are not at top level. Fixes #5510. --- src/theory/strings/regexp_entail.cpp | 12 +++++++----- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/issue5510-re-consume.smt2 | 9 +++++++++ 3 files changed, 17 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/strings/issue5510-re-consume.smt2 diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 0ab634c88..4a6df2fd8 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -252,9 +252,11 @@ Node RegExpEntail::simpleRegexpConsume(std::vector& mchildren, { if (children_s.empty()) { - // check if beyond this, we can't do it or there is nothing - // left, if so, repeat - bool can_skip = false; + // Check if beyond this, we hit a conflict. In this case, we + // must repeat. Notice that we do not treat the case where + // there are no more strings to consume as a failure, since + // we may be within a recursive call, see issue #5510. + bool can_skip = true; if (children.size() > 1) { std::vector mchildren_ss; @@ -273,9 +275,9 @@ Node RegExpEntail::simpleRegexpConsume(std::vector& mchildren, Trace("regexp-ext-rewrite-debug") << push; Node rets = simpleRegexpConsume(mchildren_ss, children_ss, t); Trace("regexp-ext-rewrite-debug") << pop; - if (rets.isNull()) + if (!rets.isNull()) { - can_skip = true; + can_skip = false; } } if (!can_skip) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1bf6c63f0..f66dc2d10 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1863,6 +1863,7 @@ set(regress_1_tests regress1/strings/issue5330_2.smt2 regress1/strings/issue5374-proxy-i.smt2 regress1/strings/issue5483-pp-leq.smt2 + regress1/strings/issue5510-re-consume.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue5510-re-consume.smt2 b/test/regress/regress1/strings/issue5510-re-consume.smt2 new file mode 100644 index 000000000..3b7aaf344 --- /dev/null +++ b/test/regress/regress1/strings/issue5510-re-consume.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_S) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(assert (str.in_re (str.++ x "B" y) (re.* (re.++ (str.to_re "A") (re.union (re.* (str.to_re "A")) (str.to_re "B")))))) +(assert (str.in_re y (str.to_re "A"))) +(check-sat) -- cgit v1.2.3 From 2576297452114b9bc916c84a748a5337e595a323 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 25 Nov 2020 01:07:42 +0100 Subject: Refactor transcendental solver (#5514) The transcendental solver has grown over time, and a refactoring was due. This PR splits the transcendental solver into five components: a utility to compute taylor approximations a common state for transcendental solvers a solver for exponential function a solver for sine function a solver that wraps everything to a transcendental solver. --- src/CMakeLists.txt | 12 +- src/theory/arith/nl/nl_lemma_utils.h | 19 + src/theory/arith/nl/nonlinear_extension.h | 4 +- .../arith/nl/transcendental/exponential_solver.cpp | 207 +++ .../arith/nl/transcendental/exponential_solver.h | 110 ++ src/theory/arith/nl/transcendental/sine_solver.cpp | 328 +++++ src/theory/arith/nl/transcendental/sine_solver.h | 177 +++ .../arith/nl/transcendental/taylor_generator.cpp | 317 +++++ .../arith/nl/transcendental/taylor_generator.h | 118 ++ .../nl/transcendental/transcendental_solver.cpp | 402 ++++++ .../nl/transcendental/transcendental_solver.h | 204 +++ .../nl/transcendental/transcendental_state.cpp | 384 +++++ .../arith/nl/transcendental/transcendental_state.h | 213 +++ src/theory/arith/nl/transcendental_solver.cpp | 1474 -------------------- src/theory/arith/nl/transcendental_solver.h | 423 ------ 15 files changed, 2491 insertions(+), 1901 deletions(-) create mode 100644 src/theory/arith/nl/transcendental/exponential_solver.cpp create mode 100644 src/theory/arith/nl/transcendental/exponential_solver.h create mode 100644 src/theory/arith/nl/transcendental/sine_solver.cpp create mode 100644 src/theory/arith/nl/transcendental/sine_solver.h create mode 100644 src/theory/arith/nl/transcendental/taylor_generator.cpp create mode 100644 src/theory/arith/nl/transcendental/taylor_generator.h create mode 100644 src/theory/arith/nl/transcendental/transcendental_solver.cpp create mode 100644 src/theory/arith/nl/transcendental/transcendental_solver.h create mode 100644 src/theory/arith/nl/transcendental/transcendental_state.cpp create mode 100644 src/theory/arith/nl/transcendental/transcendental_state.h delete mode 100644 src/theory/arith/nl/transcendental_solver.cpp delete mode 100644 src/theory/arith/nl/transcendental_solver.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 366e72af0..70cb68431 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -387,8 +387,16 @@ libcvc4_add_sources( theory/arith/nl/stats.h theory/arith/nl/strategy.cpp theory/arith/nl/strategy.h - theory/arith/nl/transcendental_solver.cpp - theory/arith/nl/transcendental_solver.h + theory/arith/nl/transcendental/exponential_solver.cpp + theory/arith/nl/transcendental/exponential_solver.h + theory/arith/nl/transcendental/sine_solver.cpp + theory/arith/nl/transcendental/sine_solver.h + theory/arith/nl/transcendental/taylor_generator.cpp + theory/arith/nl/transcendental/taylor_generator.h + theory/arith/nl/transcendental/transcendental_solver.cpp + theory/arith/nl/transcendental/transcendental_solver.h + theory/arith/nl/transcendental/transcendental_state.cpp + theory/arith/nl/transcendental/transcendental_state.h theory/arith/normal_form.cpp theory/arith/normal_form.h theory/arith/operator_elim.cpp diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index ac52e7d52..24302339c 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -98,6 +98,25 @@ struct SortNlModel bool operator()(Node i, Node j); }; +/** + * Wrapper for std::sort that uses SortNlModel to sort an iterator range. + */ +template +void sortByNlModel(It begin, + It end, + NlModel* model, + bool concrete = true, + bool absolute = false, + bool reverse = false) +{ + SortNlModel smv; + smv.d_nlm = model; + smv.d_isConcrete = concrete; + smv.d_isAbsolute = absolute; + smv.d_reverse_order = reverse; + std::sort(begin, end, smv); +} + struct SortNonlinearDegree { SortNonlinearDegree(const std::map& m) : d_mdegree(m) {} diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 21b978a55..b563384a5 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -38,7 +38,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" -#include "theory/arith/nl/transcendental_solver.h" +#include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" #include "theory/uf/equality_engine.h" @@ -253,7 +253,7 @@ class NonlinearExtension * This is the subsolver responsible for running the procedure for * transcendental functions. */ - TranscendentalSolver d_trSlv; + transcendental::TranscendentalSolver d_trSlv; /** * Holds common lookup data for the checks implemented in the "nl-ext" * solvers (from Cimatti et al., TACAS 2017). diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp new file mode 100644 index 000000000..4275b2487 --- /dev/null +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -0,0 +1,207 @@ +/********************* */ +/*! \file transcendental_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of solver for handling transcendental functions. + **/ + +#include "theory/arith/nl/transcendental/exponential_solver.h" + +#include +#include + +#include "expr/node_algorithm.h" +#include "expr/node_builder.h" +#include "options/arith_options.h" +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +ExponentialSolver::ExponentialSolver(TranscendentalState* tstate) + : d_data(tstate) +{ +} + +ExponentialSolver::~ExponentialSolver() {} + +void ExponentialSolver::checkInitialRefine() +{ + NodeManager* nm = NodeManager::currentNM(); + Trace("nl-ext") + << "Get initial refinement lemmas for transcendental functions..." + << std::endl; + for (std::pair >& tfl : d_data->d_funcMap) + { + if (tfl.first != Kind::EXPONENTIAL) + { + continue; + } + Assert(tfl.first == Kind::EXPONENTIAL); + for (const Node& t : tfl.second) + { + // initial refinements + if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end()) + { + d_tf_initial_refine[t] = true; + Node lem; + // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) < + // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 ) + lem = nm->mkNode( + Kind::AND, + nm->mkNode(Kind::GT, t, d_data->d_zero), + nm->mkNode(Kind::EQUAL, + t[0].eqNode(d_data->d_zero), + t.eqNode(d_data->d_one)), + nm->mkNode(Kind::EQUAL, + nm->mkNode(Kind::LT, t[0], d_data->d_zero), + nm->mkNode(Kind::LT, t, d_data->d_one)), + nm->mkNode( + Kind::OR, + nm->mkNode(Kind::LEQ, t[0], d_data->d_zero), + nm->mkNode( + Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one)))); + if (!lem.isNull()) + { + d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_INIT_REFINE); + } + } + } + } +} + +void ExponentialSolver::checkMonotonic() +{ + Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..." + << std::endl; + + auto it = d_data->d_funcMap.find(Kind::EXPONENTIAL); + if (it == d_data->d_funcMap.end()) + { + Trace("nl-ext-exp") << "No exponential terms" << std::endl; + return; + } + + // sort arguments of all transcendentals + std::vector tf_args; + std::map tf_arg_to_term; + + for (const Node& tf : it->second) + { + Node a = tf[0]; + Node mvaa = d_data->d_model.computeAbstractModelValue(a); + if (mvaa.isConst()) + { + Trace("nl-ext-exp") << "...tf term : " << a << std::endl; + tf_args.push_back(a); + tf_arg_to_term[a] = tf; + } + } + + if (tf_args.empty()) + { + return; + } + + sortByNlModel( + tf_args.begin(), tf_args.end(), &d_data->d_model, true, false, true); + + Node targ, targval, t, tval; + for (const auto& sarg : tf_args) + { + Node sargval = d_data->d_model.computeAbstractModelValue(sarg); + Assert(sargval.isConst()); + Node s = tf_arg_to_term[sarg]; + Node sval = d_data->d_model.computeAbstractModelValue(s); + Assert(sval.isConst()); + + // store the concavity region + d_data->d_tf_region[s] = 1; + Trace("nl-ext-concavity") << ", arg model value = " << sargval << std::endl; + + if (!tval.isNull() && sval.getConst() > tval.getConst()) + { + NodeManager* nm = NodeManager::currentNM(); + Node mono_lem = nm->mkNode(Kind::IMPLIES, + nm->mkNode(Kind::GEQ, targ, sarg), + nm->mkNode(Kind::GEQ, t, s)); + Trace("nl-ext-exp") << "Monotonicity lemma : " << mono_lem << std::endl; + + d_data->d_im.addPendingArithLemma(mono_lem, + InferenceId::NL_T_MONOTONICITY); + } + // store the previous values + targ = sarg; + targval = sargval; + t = s; + tval = sval; + } +} + +void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) +{ + NodeManager* nm = NodeManager::currentNM(); + // compute tangent plane + // Figure 3: T( x ) + // We use zero slope tangent planes, since the concavity of the Taylor + // approximation cannot be easily established. + // Tangent plane is valid in the interval [c,u). + Node lem = nm->mkNode(Kind::IMPLIES, + nm->mkNode(Kind::GEQ, e[0], c), + nm->mkNode(Kind::GEQ, e, poly_approx)); + Trace("nl-ext-exp") << "*** Tangent plane lemma (pre-rewrite): " << lem + << std::endl; + lem = Rewriter::rewrite(lem); + Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl; + Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false); + // Figure 3 : line 9 + d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); +} + +void ExponentialSolver::doSecantLemmas(TNode e, + TNode c, + TNode poly_approx, + unsigned d) +{ + d_data->doSecantLemmas(getSecantBounds(e, c, d), c, poly_approx, e, d, 1); +} + +std::pair ExponentialSolver::getSecantBounds(TNode e, + TNode c, + unsigned d) +{ + std::pair bounds = d_data->getClosestSecantPoints(e, c, d); + + // Check if we already have neighboring secant points + if (bounds.first.isNull()) + { + // pick c-1 + bounds.first = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(Kind::MINUS, c, d_data->d_one)); + } + if (bounds.second.isNull()) + { + // pick c+1 + bounds.second = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(Kind::PLUS, c, d_data->d_one)); + } + return bounds; +} + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h new file mode 100644 index 000000000..f757e5892 --- /dev/null +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -0,0 +1,110 @@ +/********************* */ +/*! \file exponential_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Solving for handling exponential function. + **/ + +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H + +#include +#include +#include +#include + +#include "expr/node.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/transcendental_state.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +/** Transcendental solver class + * + * This class implements model-based refinement schemes + * for transcendental functions, described in: + * + * - "Satisfiability Modulo Transcendental + * Functions via Incremental Linearization" by Cimatti + * et al., CADE 2017. + * + * It's main functionality are methods that implement lemma schemas below, + * which return a set of lemmas that should be sent on the output channel. + */ +class ExponentialSolver +{ + public: + ExponentialSolver(TranscendentalState* tstate); + ~ExponentialSolver(); + + void initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + + /** + * check initial refine + * + * Constructs a set of valid theory lemmas, based on + * simple facts about the exponential function. + * This mostly follows the initial axioms described in + * Section 4 of "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017. + * + * Examples: + * + * exp( x )>0 + * x<0 => exp( x )<1 + */ + void checkInitialRefine(); + + /** + * check monotonicity + * + * Constructs a set of valid theory lemmas, based on a + * lemma scheme that ensures that applications + * of the exponential function respect monotonicity. + * + * Examples: + * + * x > y => exp( x ) > exp( y ) + */ + void checkMonotonic(); + + /** Sent tangent lemma around c for e */ + void doTangentLemma(TNode e, TNode c, TNode poly_approx); + + /** Sent secant lemmas around c for e */ + void doSecantLemmas(TNode e, TNode c, TNode poly_approx, unsigned d); + + private: + /** Generate bounds for secant lemmas */ + std::pair getSecantBounds(TNode e, TNode c, unsigned d); + + /** Holds common state for transcendental solvers */ + TranscendentalState* d_data; + + /** The transcendental functions we have done initial refinements on */ + std::map d_tf_initial_refine; + +}; /* class ExponentialSolver */ + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp new file mode 100644 index 000000000..012b8e7ec --- /dev/null +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -0,0 +1,328 @@ +/********************* */ +/*! \file transcendental_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of solver for handling transcendental functions. + **/ + +#include "theory/arith/nl/transcendental/sine_solver.h" + +#include +#include + +#include "expr/node_algorithm.h" +#include "expr/node_builder.h" +#include "options/arith_options.h" +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +SineSolver::SineSolver(TranscendentalState* tstate) : d_data(tstate) {} + +SineSolver::~SineSolver() {} + +void SineSolver::checkInitialRefine() +{ + NodeManager* nm = NodeManager::currentNM(); + Trace("nl-ext") + << "Get initial refinement lemmas for transcendental functions..." + << std::endl; + for (std::pair >& tfl : d_data->d_funcMap) + { + if (tfl.first != Kind::SINE) + { + continue; + } + for (const Node& t : tfl.second) + { + // initial refinements + if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end()) + { + d_tf_initial_refine[t] = true; + Node lem; + Node symn = nm->mkNode(Kind::SINE, + nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0])); + symn = Rewriter::rewrite(symn); + // Can assume it is its own master since phase is split over 0, + // hence -pi <= t[0] <= pi implies -pi <= -t[0] <= pi. + d_data->d_trMaster[symn] = symn; + d_data->d_trSlaves[symn].insert(symn); + Assert(d_data->d_trSlaves.find(t) != d_data->d_trSlaves.end()); + std::vector children; + + lem = + nm->mkNode(Kind::AND, + // bounds + nm->mkNode(Kind::AND, + nm->mkNode(Kind::LEQ, t, d_data->d_one), + nm->mkNode(Kind::GEQ, t, d_data->d_neg_one)), + // symmetry + nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero), + // sign + nm->mkNode(Kind::EQUAL, + nm->mkNode(Kind::LT, t[0], d_data->d_zero), + nm->mkNode(Kind::LT, t, d_data->d_zero)), + // zero val + nm->mkNode(Kind::EQUAL, + nm->mkNode(Kind::GT, t[0], d_data->d_zero), + nm->mkNode(Kind::GT, t, d_data->d_zero))); + lem = nm->mkNode( + Kind::AND, + lem, + // zero tangent + nm->mkNode(Kind::AND, + nm->mkNode(Kind::IMPLIES, + nm->mkNode(Kind::GT, t[0], d_data->d_zero), + nm->mkNode(Kind::LT, t, t[0])), + nm->mkNode(Kind::IMPLIES, + nm->mkNode(Kind::LT, t[0], d_data->d_zero), + nm->mkNode(Kind::GT, t, t[0]))), + // pi tangent + nm->mkNode( + Kind::AND, + nm->mkNode( + Kind::IMPLIES, + nm->mkNode(Kind::LT, t[0], d_data->d_pi), + nm->mkNode(Kind::LT, + t, + nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))), + nm->mkNode( + Kind::IMPLIES, + nm->mkNode(Kind::GT, t[0], d_data->d_pi_neg), + nm->mkNode( + Kind::GT, + t, + nm->mkNode(Kind::MINUS, d_data->d_pi_neg, t[0]))))); + if (!lem.isNull()) + { + d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_INIT_REFINE); + } + } + } + } +} + +void SineSolver::checkMonotonic() +{ + Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..." + << std::endl; + + auto it = d_data->d_funcMap.find(Kind::SINE); + if (it == d_data->d_funcMap.end()) + { + Trace("nl-ext-exp") << "No sine terms" << std::endl; + return; + } + + // sort arguments of all transcendentals + std::vector tf_args; + std::map tf_arg_to_term; + + for (const Node& tf : it->second) + { + Node a = tf[0]; + Node mvaa = d_data->d_model.computeAbstractModelValue(a); + if (mvaa.isConst()) + { + Trace("nl-ext-tf-mono-debug") << "...tf term : " << a << std::endl; + tf_args.push_back(a); + tf_arg_to_term[a] = tf; + } + } + + if (tf_args.empty()) + { + return; + } + + sortByNlModel( + tf_args.begin(), tf_args.end(), &d_data->d_model, true, false, true); + + std::vector mpoints = {d_data->d_pi, + d_data->d_pi_2, + d_data->d_zero, + d_data->d_pi_neg_2, + d_data->d_pi_neg}; + std::vector mpoints_vals; + + // get model values for points + for (const auto& point : mpoints) + { + mpoints_vals.emplace_back(d_data->d_model.computeAbstractModelValue(point)); + Assert(mpoints_vals.back().isConst()); + } + + unsigned mdir_index = 0; + int monotonic_dir = -1; + Node mono_bounds[2]; + Node targ, targval, t, tval; + for (const auto& sarg : tf_args) + { + Node sargval = d_data->d_model.computeAbstractModelValue(sarg); + Assert(sargval.isConst()); + Node s = tf_arg_to_term[sarg]; + Node sval = d_data->d_model.computeAbstractModelValue(s); + Assert(sval.isConst()); + + // increment to the proper monotonicity region + bool increment = true; + while (increment && mdir_index < mpoints.size()) + { + increment = false; + Node pval = mpoints_vals[mdir_index]; + Assert(pval.isConst()); + if (sargval.getConst() < pval.getConst()) + { + increment = true; + Trace("nl-ext-tf-mono") + << "...increment at " << sarg << " since model value is less than " + << mpoints[mdir_index] << std::endl; + } + if (increment) + { + tval = Node::null(); + mono_bounds[1] = mpoints[mdir_index]; + mdir_index++; + monotonic_dir = regionToMonotonicityDir(mdir_index); + if (mdir_index < mpoints.size()) + { + mono_bounds[0] = mpoints[mdir_index]; + } + else + { + mono_bounds[0] = Node::null(); + } + } + } + // store the concavity region + d_data->d_tf_region[s] = mdir_index; + Trace("nl-ext-concavity") + << "Transcendental function " << s << " is in region #" << mdir_index; + Trace("nl-ext-concavity") << ", arg model value = " << sargval << std::endl; + + if (!tval.isNull()) + { + NodeManager* nm = NodeManager::currentNM(); + Node mono_lem; + if (monotonic_dir == 1 + && sval.getConst() > tval.getConst()) + { + mono_lem = nm->mkNode(Kind::IMPLIES, + nm->mkNode(Kind::GEQ, targ, sarg), + nm->mkNode(Kind::GEQ, t, s)); + } + else if (monotonic_dir == -1 + && sval.getConst() < tval.getConst()) + { + mono_lem = nm->mkNode(Kind::IMPLIES, + nm->mkNode(Kind::LEQ, targ, sarg), + nm->mkNode(Kind::LEQ, t, s)); + } + if (!mono_lem.isNull()) + { + if (!mono_bounds[0].isNull()) + { + Assert(!mono_bounds[1].isNull()); + mono_lem = nm->mkNode( + Kind::IMPLIES, + nm->mkNode(Kind::AND, + mkBounded(mono_bounds[0], targ, mono_bounds[1]), + mkBounded(mono_bounds[0], sarg, mono_bounds[1])), + mono_lem); + } + Trace("nl-ext-tf-mono") + << "Monotonicity lemma : " << mono_lem << std::endl; + + d_data->d_im.addPendingArithLemma(mono_lem, + InferenceId::NL_T_MONOTONICITY); + } + } + // store the previous values + targ = sarg; + targval = sargval; + t = s; + tval = sval; + } +} + +void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region) +{ + NodeManager* nm = NodeManager::currentNM(); + + // compute tangent plane + // Figure 3: T( x ) + // We use zero slope tangent planes, since the concavity of the Taylor + // approximation cannot be easily established. + int concavity = regionToConcavity(region); + int mdir = regionToMonotonicityDir(region); + Node lem = nm->mkNode( + Kind::IMPLIES, + nm->mkNode( + Kind::AND, + nm->mkNode(Kind::GEQ, + e[0], + mdir == concavity ? Node(c) : regionToLowerBound(region)), + nm->mkNode(Kind::LEQ, + e[0], + mdir != concavity ? Node(c) : regionToUpperBound(region))), + nm->mkNode(concavity == 1 ? Kind::GEQ : Kind::LEQ, e, poly_approx)); + + Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem + << std::endl; + lem = Rewriter::rewrite(lem); + Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl; + Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false); + // Figure 3 : line 9 + d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); +} + +void SineSolver::doSecantLemmas( + TNode e, TNode c, TNode poly_approx, unsigned d, int region) +{ + d_data->doSecantLemmas(getSecantBounds(e, c, d, region), + c, + poly_approx, + e, + d, + regionToConcavity(region)); +} + +std::pair SineSolver::getSecantBounds(TNode e, + TNode c, + unsigned d, + int region) +{ + std::pair bounds = d_data->getClosestSecantPoints(e, c, d); + + // Check if we already have neighboring secant points + if (bounds.first.isNull()) + { + // lower boundary point for this concavity region + bounds.first = regionToLowerBound(region); + } + if (bounds.second.isNull()) + { + // upper boundary point for this concavity region + bounds.second = regionToUpperBound(region); + } + return bounds; +} + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h new file mode 100644 index 000000000..394c2d927 --- /dev/null +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -0,0 +1,177 @@ +/********************* */ +/*! \file sine_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Solving for handling exponential function. + **/ + +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H + +#include +#include +#include +#include + +#include "expr/node.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/transcendental_state.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +/** Transcendental solver class + * + * This class implements model-based refinement schemes + * for transcendental functions, described in: + * + * - "Satisfiability Modulo Transcendental + * Functions via Incremental Linearization" by Cimatti + * et al., CADE 2017. + * + * It's main functionality are methods that implement lemma schemas below, + * which return a set of lemmas that should be sent on the output channel. + */ +class SineSolver +{ + public: + SineSolver(TranscendentalState* tstate); + ~SineSolver(); + + void initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + + /** + * check initial refine + * + * Constructs a set of valid theory lemmas, based on + * simple facts about the sine function. + * This mostly follows the initial axioms described in + * Section 4 of "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017. + * + * Examples: + * + * sin( x ) = -sin( -x ) + * ( PI > x > 0 ) => 0 < sin( x ) < 1 + */ + void checkInitialRefine(); + + /** + * check monotonicity + * + * Constructs a set of valid theory lemmas, based on a + * lemma scheme that ensures that applications + * of the sine function respect monotonicity. + * + * Examples: + * + * PI/2 > x > y > 0 => sin( x ) > sin( y ) + * PI > x > y > PI/2 => sin( x ) < sin( y ) + */ + void checkMonotonic(); + + /** Sent tangent lemma around c for e */ + void doTangentLemma(TNode e, TNode c, TNode poly_approx, int region); + + /** Sent secant lemmas around c for e */ + void doSecantLemmas( + TNode e, TNode c, TNode poly_approx, unsigned d, int region); + + private: + std::pair getSecantBounds(TNode e, + TNode c, + unsigned d, + int region); + + /** region to lower bound + * + * Returns the term corresponding to the lower + * bound of the region of transcendental function + * with kind k. Returns Node::null if the region + * is invalid, or there is no lower bound for the + * region. + */ + Node regionToLowerBound(int region) + { + switch (region) + { + case 1: return d_data->d_pi_2; + case 2: return d_data->d_zero; + case 3: return d_data->d_pi_neg_2; + case 4: return d_data->d_pi_neg; + default: return Node(); + } + } + + /** region to upper bound + * + * Returns the term corresponding to the upper + * bound of the region of transcendental function + * with kind k. Returns Node::null if the region + * is invalid, or there is no upper bound for the + * region. + */ + Node regionToUpperBound(int region) + { + switch (region) + { + case 1: return d_data->d_pi; + case 2: return d_data->d_pi_2; + case 3: return d_data->d_zero; + case 4: return d_data->d_pi_neg_2; + default: return Node(); + } + } + + int regionToMonotonicityDir(int region) + { + switch (region) + { + case 1: + case 4: return -1; + case 2: + case 3: return 1; + default: return 0; + } + } + int regionToConcavity(int region) + { + switch (region) + { + case 1: + case 2: return -1; + case 3: + case 4: return 1; + default: return 0; + } + } + + /** Holds common state for transcendental solvers */ + TranscendentalState* d_data; + + /** The transcendental functions we have done initial refinements on */ + std::map d_tf_initial_refine; + +}; /* class SineSolver */ + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp new file mode 100644 index 000000000..a373339e9 --- /dev/null +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -0,0 +1,317 @@ +/********************* */ +/*! \file taylor_generator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Generate taylor approximations transcendental lemmas. + **/ + +#include "theory/arith/nl/transcendental/taylor_generator.h" + +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +TaylorGenerator::TaylorGenerator() + : d_nm(NodeManager::currentNM()), + d_taylor_real_fv(d_nm->mkBoundVar("x", d_nm->realType())), + d_taylor_real_fv_base(d_nm->mkBoundVar("a", d_nm->realType())), + d_taylor_real_fv_base_rem(d_nm->mkBoundVar("b", d_nm->realType())) +{ +} + +TNode TaylorGenerator::getTaylorVariable() { return d_taylor_real_fv; } + +std::pair TaylorGenerator::getTaylor(TNode fa, std::uint64_t n) +{ + NodeManager* nm = NodeManager::currentNM(); + Node d_zero = nm->mkConst(Rational(0)); + + Assert(n > 0); + Node fac; // what term we cache for fa + if (fa[0] == d_zero) + { + // optimization : simpler to compute (x-fa[0])^n if we are centered around 0 + fac = fa; + } + else + { + // otherwise we use a standard factor a in (x-a)^n + fac = nm->mkNode(fa.getKind(), d_taylor_real_fv_base); + } + Node taylor_rem; + Node taylor_sum; + // check if we have already computed this Taylor series + auto itt = s_taylor_sum[fac].find(n); + if (itt == s_taylor_sum[fac].end()) + { + Node i_exp_base; + if (fa[0] == d_zero) + { + i_exp_base = d_taylor_real_fv; + } + else + { + i_exp_base = Rewriter::rewrite( + nm->mkNode(Kind::MINUS, d_taylor_real_fv, d_taylor_real_fv_base)); + } + Node i_derv = fac; + Node i_fact = nm->mkConst(Rational(1)); + Node i_exp = i_fact; + int i_derv_status = 0; + unsigned counter = 0; + std::vector sum; + do + { + counter++; + if (fa.getKind() == Kind::EXPONENTIAL) + { + // unchanged + } + else if (fa.getKind() == Kind::SINE) + { + if (i_derv_status % 2 == 1) + { + Node pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); + Node pi_2 = Rewriter::rewrite(nm->mkNode( + Kind::MULT, pi, nm->mkConst(Rational(1) / Rational(2)))); + + Node arg = nm->mkNode(Kind::PLUS, pi_2, d_taylor_real_fv_base); + i_derv = nm->mkNode(Kind::SINE, arg); + } + else + { + i_derv = fa; + } + if (i_derv_status >= 2) + { + i_derv = nm->mkNode(Kind::MINUS, d_zero, i_derv); + } + i_derv = Rewriter::rewrite(i_derv); + i_derv_status = i_derv_status == 3 ? 0 : i_derv_status + 1; + } + if (counter == (n + 1)) + { + TNode x = d_taylor_real_fv_base; + i_derv = i_derv.substitute(x, d_taylor_real_fv_base_rem); + } + Node curr = nm->mkNode( + Kind::MULT, nm->mkNode(Kind::DIVISION, i_derv, i_fact), i_exp); + if (counter == (n + 1)) + { + taylor_rem = curr; + } + else + { + sum.push_back(curr); + i_fact = Rewriter::rewrite( + nm->mkNode(Kind::MULT, nm->mkConst(Rational(counter)), i_fact)); + i_exp = Rewriter::rewrite(nm->mkNode(Kind::MULT, i_exp_base, i_exp)); + } + } while (counter <= n); + taylor_sum = sum.size() == 1 ? sum[0] : nm->mkNode(Kind::PLUS, sum); + + if (fac[0] != d_taylor_real_fv_base) + { + TNode x = d_taylor_real_fv_base; + taylor_sum = taylor_sum.substitute(x, fac[0]); + } + + // cache + s_taylor_sum[fac][n] = taylor_sum; + d_taylor_rem[fac][n] = taylor_rem; + } + else + { + taylor_sum = itt->second; + Assert(d_taylor_rem[fac].find(n) != d_taylor_rem[fac].end()); + taylor_rem = d_taylor_rem[fac][n]; + } + + // must substitute for the argument if we were using a different lookup + if (fa[0] != fac[0]) + { + TNode x = d_taylor_real_fv_base; + taylor_sum = taylor_sum.substitute(x, fa[0]); + } + return std::pair(taylor_sum, taylor_rem); +} + +void TaylorGenerator::getPolynomialApproximationBounds( + Kind k, unsigned d, std::vector& pbounds) +{ + if (d_poly_bounds[k][d].empty()) + { + NodeManager* nm = NodeManager::currentNM(); + Node tft = nm->mkNode(k, nm->mkConst(Rational(0))); + // n is the Taylor degree we are currently considering + unsigned n = 2 * d; + // n must be even + std::pair taylor = getTaylor(tft, n); + Trace("nl-ext-tftp-debug2") + << "Taylor for " << k << " is : " << taylor.first << std::endl; + Node taylor_sum = Rewriter::rewrite(taylor.first); + Trace("nl-ext-tftp-debug2") + << "Taylor for " << k << " is (post-rewrite) : " << taylor_sum + << std::endl; + Assert(taylor.second.getKind() == Kind::MULT); + Assert(taylor.second.getNumChildren() == 2); + Assert(taylor.second[0].getKind() == Kind::DIVISION); + Trace("nl-ext-tftp-debug2") + << "Taylor remainder for " << k << " is " << taylor.second << std::endl; + // ru is x^{n+1}/(n+1)! + Node ru = nm->mkNode(Kind::DIVISION, taylor.second[1], taylor.second[0][1]); + ru = Rewriter::rewrite(ru); + Trace("nl-ext-tftp-debug2") + << "Taylor remainder factor is (post-rewrite) : " << ru << std::endl; + if (k == Kind::EXPONENTIAL) + { + pbounds.push_back(taylor_sum); + pbounds.push_back(taylor_sum); + pbounds.push_back(Rewriter::rewrite( + nm->mkNode(Kind::MULT, + taylor_sum, + nm->mkNode(Kind::PLUS, nm->mkConst(Rational(1)), ru)))); + pbounds.push_back( + Rewriter::rewrite(nm->mkNode(Kind::PLUS, taylor_sum, ru))); + } + else + { + Assert(k == Kind::SINE); + Node l = Rewriter::rewrite(nm->mkNode(Kind::MINUS, taylor_sum, ru)); + Node u = Rewriter::rewrite(nm->mkNode(Kind::PLUS, taylor_sum, ru)); + pbounds.push_back(l); + pbounds.push_back(l); + pbounds.push_back(u); + pbounds.push_back(u); + } + Trace("nl-ext-tf-tplanes") + << "Polynomial approximation for " << k << " is: " << std::endl; + Trace("nl-ext-tf-tplanes") << " Lower (pos): " << pbounds[0] << std::endl; + Trace("nl-ext-tf-tplanes") << " Upper (pos): " << pbounds[2] << std::endl; + Trace("nl-ext-tf-tplanes") << " Lower (neg): " << pbounds[1] << std::endl; + Trace("nl-ext-tf-tplanes") << " Upper (neg): " << pbounds[3] << std::endl; + d_poly_bounds[k][d].insert( + d_poly_bounds[k][d].end(), pbounds.begin(), pbounds.end()); + } + else + { + pbounds.insert( + pbounds.end(), d_poly_bounds[k][d].begin(), d_poly_bounds[k][d].end()); + } +} + +void TaylorGenerator::getPolynomialApproximationBoundForArg( + Kind k, Node c, unsigned d, std::vector& pbounds) +{ + getPolynomialApproximationBounds(k, d, pbounds); + Assert(c.isConst()); + if (k == Kind::EXPONENTIAL && c.getConst().sgn() == 1) + { + NodeManager* nm = NodeManager::currentNM(); + Node tft = nm->mkNode(k, nm->mkConst(Rational(0))); + bool success = false; + unsigned ds = d; + TNode ttrf = getTaylorVariable(); + TNode tc = c; + do + { + success = true; + unsigned n = 2 * ds; + std::pair taylor = getTaylor(tft, n); + // check that 1-c^{n+1}/(n+1)! > 0 + Node ru = + nm->mkNode(Kind::DIVISION, taylor.second[1], taylor.second[0][1]); + Node rus = ru.substitute(ttrf, tc); + rus = Rewriter::rewrite(rus); + Assert(rus.isConst()); + if (rus.getConst() > 1) + { + success = false; + ds = ds + 1; + } + } while (!success); + if (ds > d) + { + Trace("nl-ext-exp-taylor") + << "*** Increase Taylor bound to " << ds << " > " << d << " for (" + << k << " " << c << ")" << std::endl; + // must use sound upper bound + std::vector pboundss; + getPolynomialApproximationBounds(k, ds, pboundss); + pbounds[2] = pboundss[2]; + } + } +} + +std::pair TaylorGenerator::getTfModelBounds(Node tf, unsigned d, NlModel& model) +{ + // compute the model value of the argument + Node c = model.computeAbstractModelValue(tf[0]); + Assert(c.isConst()); + int csign = c.getConst().sgn(); + Kind k = tf.getKind(); + if (csign == 0) + { + NodeManager* nm = NodeManager::currentNM(); + // at zero, its trivial + if (k == Kind::SINE) + { + Node zero = nm->mkConst(Rational(0)); + return std::pair(zero, zero); + } + Assert(k == Kind::EXPONENTIAL); + Node one = nm->mkConst(Rational(1)); + return std::pair(one, one); + } + bool isNeg = csign == -1; + + std::vector pbounds; + getPolynomialApproximationBoundForArg(k, c, d, pbounds); + + std::vector bounds; + TNode tfv = getTaylorVariable(); + TNode tfs = tf[0]; + for (unsigned d2 = 0; d2 < 2; d2++) + { + int index = d2 == 0 ? (isNeg ? 1 : 0) : (isNeg ? 3 : 2); + Node pab = pbounds[index]; + if (!pab.isNull()) + { + // { x -> M_A(tf[0]) } + // Notice that we compute the model value of tfs first, so that + // the call to rewrite below does not modify the term, where notice that + // rewrite( x*x { x -> M_A(t) } ) = M_A(t)*M_A(t) + // is not equal to + // M_A( x*x { x -> t } ) = M_A( t*t ) + // where M_A denotes the abstract model. + Node mtfs = model.computeAbstractModelValue(tfs); + pab = pab.substitute(tfv, mtfs); + pab = Rewriter::rewrite(pab); + Assert(pab.isConst()); + bounds.push_back(pab); + } + else + { + bounds.push_back(Node::null()); + } + } + return std::pair(bounds[0], bounds[1]); +} + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h new file mode 100644 index 000000000..c647f7fd2 --- /dev/null +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \file taylor_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Generate taylor approximations transcendental lemmas. + **/ + +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H + +#include "expr/node.h" +#include "theory/arith/nl/nl_model.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +class TaylorGenerator +{ + public: + TaylorGenerator(); + + /** + * Return the variable used as x in getTaylor(). + */ + TNode getTaylorVariable(); + + /** + * Get Taylor series of degree n for function fa centered around point fa[0]. + * + * Return value is ( P_{n,f(a)}( x ), R_{n+1,f(a)}( x ) ) where + * the first part of the pair is the Taylor series expansion : + * P_{n,f(a)}( x ) = sum_{i=0}^n (f^i( a )/i!)*(x-a)^i + * and the second part of the pair is the Taylor series remainder : + * R_{n+1,f(a),b}( x ) = (f^{n+1}( b )/(n+1)!)*(x-a)^{n+1} + * + * The above values are cached for each (f,n) for a fixed variable "a". + * To compute the Taylor series for fa, we compute the Taylor series + * for ( fa.getKind(), n ) then substitute { a -> fa[0] } if fa[0]!=0. + * We compute P_{n,f(0)}( x )/R_{n+1,f(0),b}( x ) for ( fa.getKind(), n ) + * if fa[0]=0. + * In the latter case, note we compute the exponential x^{n+1} + * instead of (x-a)^{n+1}, which can be done faster. + */ + std::pair getTaylor(TNode fa, std::uint64_t n); + + /** + * polynomial approximation bounds + * + * This adds P_l+[x], P_l-[x], P_u+[x], P_u-[x] to pbounds, where x is + * d_taylor_real_fv. These are polynomial approximations of the Taylor series + * of ( 0 ) for degree 2*d where k is SINE or EXPONENTIAL. + * These correspond to P_l and P_u from Figure 3 of Cimatti et al., CADE 2017, + * for positive/negative (+/-) values of the argument of ( 0 ). + * + * Notice that for certain bounds (e.g. upper bounds for exponential), the + * Taylor approximation for a fixed degree is only sound up to a given + * upper bound on the argument. To obtain sound lower/upper bounds for a + * given ( c ), use the function below. + */ + void getPolynomialApproximationBounds(Kind k, + unsigned d, + std::vector& pbounds); + + /** + * polynomial approximation bounds + * + * This computes polynomial approximations P_l+[x], P_l-[x], P_u+[x], P_u-[x] + * that are sound (lower, upper) bounds for ( c ). Notice that these + * polynomials may depend on c. In particular, for P_u+[x] for ( c ) where + * c>0, we return the P_u+[x] from the function above for the minimum degree + * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive. + */ + void getPolynomialApproximationBoundForArg(Kind k, + Node c, + unsigned d, + std::vector& pbounds); + + /** get transcendental function model bounds + * + * This returns the current lower and upper bounds of transcendental + * function application tf based on Taylor of degree 2*d, which is dependent + * on the model value of its argument. + */ + std::pair getTfModelBounds(Node tf, unsigned d, NlModel& model); + + private: + NodeManager* d_nm; + const Node d_taylor_real_fv; + const Node d_taylor_real_fv_base; + const Node d_taylor_real_fv_base_rem; + std::unordered_map, + NodeHashFunction> + s_taylor_sum; + std::unordered_map, + NodeHashFunction> + d_taylor_rem; + std::map>> d_poly_bounds; +}; + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp new file mode 100644 index 000000000..1f76cd833 --- /dev/null +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -0,0 +1,402 @@ +/********************* */ +/*! \file transcendental_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of solver for handling transcendental functions. + **/ + +#include "theory/arith/nl/transcendental/transcendental_solver.h" + +#include +#include + +#include "expr/node_algorithm.h" +#include "expr/node_builder.h" +#include "options/arith_options.h" +#include "theory/arith/arith_msum.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/transcendental/taylor_generator.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +TranscendentalSolver::TranscendentalSolver(InferenceManager& im, NlModel& m) + : d_tstate(im, m), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) +{ + d_taylor_degree = options::nlExtTfTaylorDegree(); +} + +TranscendentalSolver::~TranscendentalSolver() {} + +void TranscendentalSolver::initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts) +{ + d_tstate.init(assertions, false_asserts, xts); +} + +bool TranscendentalSolver::preprocessAssertionsCheckModel( + std::vector& assertions) +{ + std::vector pvars; + std::vector psubs; + for (const std::pair& tb : d_tstate.d_trMaster) + { + pvars.push_back(tb.first); + psubs.push_back(tb.second); + } + + // initialize representation of assertions + std::vector passertions; + for (const Node& a : assertions) + + { + Node pa = a; + if (!pvars.empty()) + { + pa = arithSubstitute(pa, pvars, psubs); + pa = Rewriter::rewrite(pa); + } + if (!pa.isConst() || !pa.getConst()) + { + Trace("nl-ext-cm-assert") << "- assert : " << pa << std::endl; + passertions.push_back(pa); + } + } + // get model bounds for all transcendental functions + Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..." + << std::endl; + for (std::pair >& tfs : d_tstate.d_funcMap) + { + for (const Node& tf : tfs.second) + { + Trace("nl-ext-cm") << "- Term: " << tf << std::endl; + bool success = true; + // tf is Figure 3 : tf( x ) + std::pair bounds; + if (tfs.first == Kind::PI) + { + bounds = {d_tstate.d_pi_bound[0], d_tstate.d_pi_bound[1]}; + } + else + { + bounds = d_tstate.d_taylor.getTfModelBounds( + tf, d_taylor_degree, d_tstate.d_model); + if (bounds.first != bounds.second) + { + d_tstate.d_model.setUsedApproximate(); + } + } + if (!bounds.first.isNull() && !bounds.second.isNull()) + { + // for each function in the congruence classe + for (const Node& ctf : d_tstate.d_funcCongClass[tf]) + { + // each term in congruence classes should be master terms + Assert(d_tstate.d_trSlaves.find(ctf) != d_tstate.d_trSlaves.end()); + // we set the bounds for each slave of tf + for (const Node& stf : d_tstate.d_trSlaves[ctf]) + { + Trace("nl-ext-cm") + << "...bound for " << stf << " : [" << bounds.first << ", " + << bounds.second << "]" << std::endl; + success = d_tstate.d_model.addCheckModelBound( + stf, bounds.first, bounds.second); + } + } + } + else + { + Trace("nl-ext-cm") << "...no bound for " << tf << std::endl; + } + if (!success) + { + // a bound was conflicting + Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl; + Trace("nl-ext-cm") << "-----" << std::endl; + return false; + } + } + } + // replace the assertions + assertions = std::move(passertions); + return true; +} + +void TranscendentalSolver::incrementTaylorDegree() { d_taylor_degree++; } +unsigned TranscendentalSolver::getTaylorDegree() const +{ + return d_taylor_degree; +} + +void TranscendentalSolver::processSideEffect(const NlLemma& se) +{ + for (const std::tuple& sp : se.d_secantPoint) + { + Node tf = std::get<0>(sp); + unsigned d = std::get<1>(sp); + Node c = std::get<2>(sp); + d_tstate.d_secant_points[tf][d].push_back(c); + } +} + +void TranscendentalSolver::checkTranscendentalInitialRefine() +{ + d_expSlv.checkInitialRefine(); + d_sineSlv.checkInitialRefine(); +} + +void TranscendentalSolver::checkTranscendentalMonotonic() +{ + d_expSlv.checkMonotonic(); + d_sineSlv.checkMonotonic(); +} + +void TranscendentalSolver::checkTranscendentalTangentPlanes() +{ + Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..." + << std::endl; + // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions + // via Incremental Linearization" by Cimatti et al + for (const std::pair >& tfs : + d_tstate.d_funcMap) + { + Kind k = tfs.first; + if (k == PI) + { + // We do not use Taylor approximation for PI currently. + // This is because the convergence is extremely slow, and hence an + // initial approximation is superior. + continue; + } + + // we substitute into the Taylor sum P_{n,f(0)}( x ) + + for (const Node& tf : tfs.second) + { + // tf is Figure 3 : tf( x ) + 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 = + d_tstate.d_im.numPendingLemmas() + d_tstate.d_im.numWaitingLemmas(); + if (checkTfTangentPlanesFun(tf, d)) + { + Trace("nl-ext-tftp") << "...fail, #lemmas = " + << (d_tstate.d_im.numPendingLemmas() + + d_tstate.d_im.numWaitingLemmas() - prev) + << std::endl; + break; + } + else + { + Trace("nl-ext-tftp") << "...success" << std::endl; + } + } + } + } +} + +bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) +{ + NodeManager* nm = NodeManager::currentNM(); + Kind k = tf.getKind(); + // this should only be run on master applications + Assert(d_tstate.d_trSlaves.find(tf) != d_tstate.d_trSlaves.end()); + + // Figure 3 : c + Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]); + int csign = c.getConst().sgn(); + if (csign == 0) + { + // no secant/tangent plane is necessary + return true; + } + Assert(csign == 1 || csign == -1); + + // Figure 3: P_l, P_u + // mapped to for signs of c + std::map poly_approx_bounds[2]; + std::vector pbounds; + d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds); + poly_approx_bounds[0][1] = pbounds[0]; + poly_approx_bounds[0][-1] = pbounds[1]; + poly_approx_bounds[1][1] = pbounds[2]; + poly_approx_bounds[1][-1] = pbounds[3]; + + // Figure 3 : v + Node v = d_tstate.d_model.computeAbstractModelValue(tf); + + // check value of tf + Trace("nl-ext-tftp-debug") << "Process tangent plane refinement for " << tf + << ", degree " << d << "..." << std::endl; + Trace("nl-ext-tftp-debug") << " value in model : " << v << std::endl; + Trace("nl-ext-tftp-debug") << " arg value in model : " << c << std::endl; + + // compute the concavity + int region = -1; + std::unordered_map::iterator itr = + d_tstate.d_tf_region.find(tf); + if (itr != d_tstate.d_tf_region.end()) + { + region = itr->second; + Trace("nl-ext-tftp-debug") << " region is : " << region << std::endl; + } + // Figure 3 : conc + int concavity = regionToConcavity(k, itr->second); + Trace("nl-ext-tftp-debug") << " concavity is : " << concavity << std::endl; + if (concavity == 0) + { + // no secant/tangent plane is necessary + return true; + } + + // Figure 3: P + Node poly_approx; + + // compute whether this is a tangent refinement or a secant refinement + bool is_tangent = false; + bool is_secant = false; + std::pair mvb = + d_tstate.d_taylor.getTfModelBounds(tf, d, d_tstate.d_model); + // this is the approximated value of tf(c), which is a value such that: + // M_A(tf(c)) >= poly_appox_c >= tf(c) or + // M_A(tf(c)) <= poly_appox_c <= tf(c) + // In other words, it is a better approximation of the true value of tf(c) + // in the case that we add a refinement lemma. We use this value in the + // refinement schemas below. + Node poly_approx_c; + for (unsigned r = 0; r < 2; r++) + { + Node pab = poly_approx_bounds[r][csign]; + Node v_pab = r == 0 ? mvb.first : mvb.second; + if (!v_pab.isNull()) + { + Trace("nl-ext-tftp-debug2") + << "...model value of " << pab << " is " << v_pab << std::endl; + + Assert(v_pab.isConst()); + Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab); + Trace("nl-ext-tftp-debug2") << "...compare : " << comp << std::endl; + Node compr = Rewriter::rewrite(comp); + Trace("nl-ext-tftp-debug2") << "...got : " << compr << std::endl; + if (compr == d_tstate.d_true) + { + poly_approx_c = Rewriter::rewrite(v_pab); + // beyond the bounds + if (r == 0) + { + poly_approx = poly_approx_bounds[r][csign]; + is_tangent = concavity == 1; + is_secant = concavity == -1; + } + else + { + poly_approx = poly_approx_bounds[r][csign]; + is_tangent = concavity == -1; + is_secant = concavity == 1; + } + if (Trace.isOn("nl-ext-tftp")) + { + Trace("nl-ext-tftp") << "*** Outside boundary point ("; + Trace("nl-ext-tftp") << (r == 0 ? "low" : "high") << ") "; + printRationalApprox("nl-ext-tftp", v_pab); + Trace("nl-ext-tftp") << ", will refine..." << std::endl; + Trace("nl-ext-tftp") + << " poly_approx = " << poly_approx << std::endl; + Trace("nl-ext-tftp") + << " is_tangent = " << is_tangent << std::endl; + Trace("nl-ext-tftp") << " is_secant = " << is_secant << std::endl; + } + break; + } + else + { + Trace("nl-ext-tftp") + << " ...within " << (r == 0 ? "low" : "high") << " bound : "; + printRationalApprox("nl-ext-tftp", v_pab); + Trace("nl-ext-tftp") << std::endl; + } + } + } + + // Figure 3: P( c ) + if (is_tangent || is_secant) + { + Trace("nl-ext-tftp-debug2") + << "...poly approximation at c is " << poly_approx_c << std::endl; + } + else + { + // we may want to continue getting better bounds + return false; + } + + if (is_tangent) + { + if (k == Kind::EXPONENTIAL) + { + d_expSlv.doTangentLemma(tf, c, poly_approx_c); + } + else if (k == Kind::SINE) + { + d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region); + } + } + else if (is_secant) + { + if (k == EXPONENTIAL) + { + d_expSlv.doSecantLemmas(tf, c, poly_approx_c, d); + } + else if (k == Kind::SINE) + { + d_sineSlv.doSecantLemmas(tf, c, poly_approx_c, d, region); + } + } + return true; +} + +int TranscendentalSolver::regionToConcavity(Kind k, int region) +{ + if (k == EXPONENTIAL) + { + if (region == 1) + { + return 1; + } + } + else if (k == SINE) + { + if (region == 1 || region == 2) + { + return -1; + } + else if (region == 3 || region == 4) + { + return 1; + } + } + return 0; +} + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h new file mode 100644 index 000000000..b0db79b6a --- /dev/null +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -0,0 +1,204 @@ + +/********************* */ +/*! \file transcendental_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Solving for handling transcendental functions. + **/ + +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H + +#include +#include +#include +#include + +#include "expr/node.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/exponential_solver.h" +#include "theory/arith/nl/transcendental/sine_solver.h" +#include "theory/arith/nl/transcendental/transcendental_state.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +/** Transcendental solver class + * + * This class implements model-based refinement schemes + * for transcendental functions, described in: + * + * - "Satisfiability Modulo Transcendental + * Functions via Incremental Linearization" by Cimatti + * et al., CADE 2017. + * + * It's main functionality are methods that implement lemma schemas below, + * which return a set of lemmas that should be sent on the output channel. + */ +class TranscendentalSolver +{ + public: + TranscendentalSolver(InferenceManager& im, NlModel& m); + ~TranscendentalSolver(); + + /** init last call + * + * This is called at the beginning of last call effort check, where + * assertions are the set of assertions belonging to arithmetic, + * false_asserts is the subset of assertions that are false in the current + * model, and xts is the set of extended function terms that are active in + * the current context. + * + * This call may add lemmas to lems based on registering term + * information (for example, purification of sine terms). + */ + void initLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + /** increment taylor degree */ + void incrementTaylorDegree(); + /** get taylor degree */ + unsigned getTaylorDegree() const; + /** preprocess assertions check model + * + * This modifies the given assertions in preparation for running a call + * to check model. + * + * This method returns false if a bound for a transcendental function + * was conflicting. + */ + bool preprocessAssertionsCheckModel(std::vector& assertions); + /** Process side effects in lemma se */ + void processSideEffect(const NlLemma& se); + //-------------------------------------------- lemma schemas + // Relays to exp and sine solvers. + void checkTranscendentalInitialRefine(); + + // Relays to exp and sine solvers. + void checkTranscendentalMonotonic(); + + /** check transcendental tangent planes + * + * Constructs a set of valid theory lemmas, based on + * computing an "incremental linearization" of + * transcendental functions based on the model values + * of transcendental functions and their arguments. + * It is based on Figure 3 of "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017. + * This schema is not terminating in general. + * It is not enabled by default, and can + * be enabled by --nl-ext-tf-tplanes. + * + * Example: + * + * Assume we have a term sin(y) where M( y ) = 1 where M is the current model. + * Note that: + * sin(1) ~= .841471 + * + * The Taylor series and remainder of sin(y) of degree 7 is + * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5 + * R_{7,sin(0),b}( x ) = (-1/5040)*x^7 + * + * This gives us lower and upper bounds : + * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x ) + * ...where note P_u( 1 ) = 4243/5040 ~= .841865 + * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x ) + * ...where note P_l( 1 ) = 4241/5040 ~= .841468 + * + * Assume that M( sin(y) ) > P_u( 1 ). + * Since the concavity of sine in the region 0 < x < PI/2 is -1, + * we add a tangent plane refinement. + * The tangent plane at the point 1 in P_u is + * given by the formula: + * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 ) + * We add the lemma: + * ( 0 < y < PI/2 ) => sin( y ) <= T( y ) + * which is: + * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506) + * + * Assume that M( sin(y) ) < P_u( 1 ). + * Since the concavity of sine in the region 0 < x < PI/2 is -1, + * we add a secant plane refinement for some constants ( l, u ) + * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose + * l = 0 and u = M( PI/2 ) = 150517/47912. + * The secant planes at point 1 for P_l + * are given by the formulas: + * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l ) + * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u ) + * We add the lemmas: + * ( 0 < y < 1 ) => sin( y ) >= S_l( y ) + * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y ) + * which are: + * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y + * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2) + * where c1, c2 are rationals (for brevity, omitted here) + * such that c1 ~= .277 and c2 ~= 2.032. + */ + void checkTranscendentalTangentPlanes(); + + private: + /** check transcendental function refinement for tf + * + * 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, which includes the side effect of the lemma + * (if one exists). + * + * It returns false if the bounds are not precise enough to add a + * secant or tangent plane lemma. + */ + bool checkTfTangentPlanesFun(Node tf, unsigned d); + //-------------------------------------------- end lemma schemas + + /** get concavity + * + * Returns whether we are concave (+1) or convex (-1) + * in region of transcendental function with kind k, + * where region is defined above. + * Returns 0 if region is invalid. + */ + int regionToConcavity(Kind k, int region); + + /** taylor degree + * + * Indicates that the degree of the polynomials in the Taylor approximation of + * all transcendental functions is 2*d_taylor_degree. This value is set + * initially to options::nlExtTfTaylorDegree() and may be incremented + * if the option options::nlExtTfIncPrecision() is enabled. + */ + unsigned d_taylor_degree; + + /** Common state for transcendental solver */ + transcendental::TranscendentalState d_tstate; + /** The solver responsible for the exponential function */ + transcendental::ExponentialSolver d_expSlv; + /** The solver responsible for the sine function */ + transcendental::SineSolver d_sineSlv; +}; /* class TranscendentalSolver */ + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp new file mode 100644 index 000000000..b6882d606 --- /dev/null +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -0,0 +1,384 @@ +/********************* */ +/*! \file transcendental_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of solver for handling transcendental functions. + **/ + +#include "theory/arith/nl/transcendental/transcendental_state.h" + +#include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/transcendental/taylor_generator.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +namespace { + +/** + * Ensure a is in the main phase: + * -pi <= a <= pi + */ +inline Node mkValidPhase(TNode a, TNode pi) +{ + return mkBounded( + NodeManager::currentNM()->mkNode(Kind::MULT, mkRationalNode(-1), pi), + a, + pi); +} +} // namespace + +TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model) + : d_im(im), d_model(model) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_one = NodeManager::currentNM()->mkConst(Rational(1)); + d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); +} + +void TranscendentalState::init(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts) +{ + d_funcCongClass.clear(); + d_funcMap.clear(); + d_tf_region.clear(); + + NodeManager* nm = NodeManager::currentNM(); + + // register the extended function terms + std::vector trNeedsMaster; + bool needPi = false; + // for computing congruence + std::map argTrie; + for (unsigned i = 0, xsize = xts.size(); i < xsize; i++) + { + Node a = xts[i]; + 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 == Kind::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].insert(a); + } + } + } + if (ak == Kind::EXPONENTIAL || ak == Kind::SINE) + { + needPi = needPi || (ak == Kind::SINE); + // if we didn't indicate that it should be purified above + if (consider) + { + std::vector repList; + for (const Node& ac : a) + { + Node r = d_model.computeConcreteModelValue(ac); + repList.push_back(r); + } + Node aa = argTrie[ak].add(a, repList); + if (aa != a) + { + // apply congruence to pairs of terms that are disequal and congruent + Assert(aa.getNumChildren() == a.getNumChildren()); + Node mvaa = d_model.computeAbstractModelValue(a); + Node mvaaa = d_model.computeAbstractModelValue(aa); + if (mvaa != mvaaa) + { + std::vector exp; + for (unsigned j = 0, size = a.getNumChildren(); j < size; j++) + { + exp.push_back(a[j].eqNode(aa[j])); + } + Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp); + Node cong_lemma = nm->mkNode(Kind::OR, expn.negate(), a.eqNode(aa)); + d_im.addPendingArithLemma(cong_lemma, InferenceId::NL_CONGRUENCE); + } + } + else + { + // new representative of congruence class + d_funcMap[ak].push_back(a); + } + // add to congruence class + d_funcCongClass[aa].push_back(a); + } + } + else if (ak == Kind::PI) + { + Assert(consider); + needPi = true; + d_funcMap[ak].push_back(a); + d_funcCongClass[a].push_back(a); + } + } + // initialize pi if necessary + if (needPi && d_pi.isNull()) + { + mkPi(); + getCurrentPiBounds(); + } + + if (d_im.hasUsed()) + { + return; + } + + // process SINE phase shifting + 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 == Kind::SINE || k == Kind::EXPONENTIAL); + Node y = + nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg"); + Node new_a = nm->mkNode(k, y); + d_trSlaves[new_a].insert(new_a); + d_trSlaves[new_a].insert(a); + d_trMaster[a] = new_a; + d_trMaster[new_a] = new_a; + Node lem; + if (k == Kind::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( + Kind::AND, + transcendental::mkValidPhase(y, d_pi), + nm->mkNode( + Kind::ITE, + transcendental::mkValidPhase(a[0], d_pi), + a[0].eqNode(y), + a[0].eqNode(nm->mkNode( + Kind::PLUS, + y, + nm->mkNode( + Kind::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(Kind::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; + NlLemma nlem( + lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG); + d_im.addPendingArithLemma(nlem); + } + + if (Trace.isOn("nl-ext-mv")) + { + Trace("nl-ext-mv") << "Arguments of trancendental functions : " + << std::endl; + for (std::pair >& tfl : d_funcMap) + { + Kind k = tfl.first; + if (k == Kind::SINE || k == Kind::EXPONENTIAL) + { + for (const Node& tf : tfl.second) + { + Node v = tf[0]; + d_model.computeConcreteModelValue(v); + d_model.computeAbstractModelValue(v); + d_model.printModelValue("nl-ext-mv", v); + } + } + } + } +} + +void TranscendentalState::mkPi() +{ + NodeManager* nm = NodeManager::currentNM(); + if (d_pi.isNull()) + { + d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); + d_pi_2 = Rewriter::rewrite( + nm->mkNode(Kind::MULT, d_pi, nm->mkConst(Rational(1) / Rational(2)))); + d_pi_neg_2 = Rewriter::rewrite( + nm->mkNode(Kind::MULT, d_pi, nm->mkConst(Rational(-1) / Rational(2)))); + d_pi_neg = Rewriter::rewrite( + nm->mkNode(Kind::MULT, d_pi, nm->mkConst(Rational(-1)))); + // initialize bounds + d_pi_bound[0] = nm->mkConst(Rational(103993) / Rational(33102)); + d_pi_bound[1] = nm->mkConst(Rational(104348) / Rational(33215)); + } +} + +void TranscendentalState::getCurrentPiBounds() +{ + NodeManager* nm = NodeManager::currentNM(); + Node pi_lem = nm->mkNode(Kind::AND, + nm->mkNode(Kind::GEQ, d_pi, d_pi_bound[0]), + nm->mkNode(Kind::LEQ, d_pi, d_pi_bound[1])); + d_im.addPendingArithLemma(pi_lem, InferenceId::NL_T_PI_BOUND); +} + +std::pair TranscendentalState::getClosestSecantPoints(TNode e, + TNode c, + unsigned d) +{ + // bounds are the minimum and maximum previous secant points + // should not repeat secant points: secant lemmas should suffice to + // rule out previous assignment + Assert( + std::find(d_secant_points[e][d].begin(), d_secant_points[e][d].end(), c) + == d_secant_points[e][d].end()); + // Insert into the (temporary) vector. We do not update this vector + // until we are sure this secant plane lemma has been processed. We do + // this by mapping the lemma to a side effect below. + std::vector spoints = d_secant_points[e][d]; + spoints.push_back(c); + + // sort + sortByNlModel(spoints.begin(), spoints.end(), &d_model); + // get the resulting index of c + unsigned index = + std::find(spoints.begin(), spoints.end(), c) - spoints.begin(); + + // bounds are the next closest upper/lower bound values + return {index > 0 ? spoints[index - 1] : Node(), + index < spoints.size() - 1 ? spoints[index + 1] : Node()}; +} + +Node TranscendentalState::mkSecantPlane( + TNode arg, TNode b, TNode c, TNode approx, TNode approx_c) +{ + NodeManager* nm = NodeManager::currentNM(); + // Figure 3 : P(l), P(u), for s = 0,1 + Node approx_b = + Rewriter::rewrite(approx.substitute(d_taylor.getTaylorVariable(), b)); + // Figure 3: S_l( x ), S_u( x ) for s = 0,1 + Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, b, c)); + Assert(rcoeff_n.isConst()); + Rational rcoeff = rcoeff_n.getConst(); + Assert(rcoeff.sgn() != 0); + return nm->mkNode(Kind::PLUS, + approx_b, + nm->mkNode(Kind::MULT, + nm->mkNode(Kind::MINUS, approx_b, approx_c), + nm->mkConst(rcoeff.inverse()), + nm->mkNode(Kind::MINUS, arg, b))); +} + +NlLemma TranscendentalState::mkSecantLemma( + TNode lower, TNode upper, int concavity, TNode tf, TNode splane) +{ + NodeManager* nm = NodeManager::currentNM(); + // With respect to Figure 3, this is slightly different. + // In particular, we chose b to be the model value of bounds[s], + // which is a constant although bounds[s] may not be (e.g. if it + // contains PI). + // To ensure that c...b does not cross an inflection point, + // we guard with the symbolic version of bounds[s]. + // This leads to lemmas e.g. of this form: + // ( c <= x <= PI/2 ) => ( sin(x) < ( P( b ) - P( c ) )*( x - + // b ) + P( b ) ) + // where b = (PI/2)^M, the current value of PI/2 in the model. + // This is sound since we are guarded by the symbolic + // representation of PI/2. + Node antec_n = nm->mkNode(Kind::AND, + nm->mkNode(Kind::GEQ, tf[0], lower), + nm->mkNode(Kind::LEQ, tf[0], upper)); + Node lem = nm->mkNode( + Kind::IMPLIES, + antec_n, + nm->mkNode(concavity == 1 ? Kind::LEQ : Kind::GEQ, tf, splane)); + Trace("nl-ext-tftp-debug2") + << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl; + lem = Rewriter::rewrite(lem); + Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl; + Assert(d_model.computeAbstractModelValue(lem) == d_false); + return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT); +} + +void TranscendentalState::doSecantLemmas(const std::pair& bounds, + TNode c, + TNode approx_c, + TNode tf, + unsigned d, + int concavity) +{ + // take the model value of l or u (since may contain PI) + // Make secant from bounds.first to c + Node lval = d_model.computeAbstractModelValue(bounds.first); + if (lval != c) + { + Node splane = mkSecantPlane(tf[0], lval, c, bounds.first, approx_c); + NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane); + // The side effect says that if lem is added, then we should add the + // secant point c for (tf,d). + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + d_im.addPendingArithLemma(nlem, true); + } + + // Make secant from c to bounds.second + Node uval = d_model.computeAbstractModelValue(bounds.second); + if (c != uval) + { + Node splane = mkSecantPlane(tf[0], c, uval, approx_c, bounds.second); + NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane); + // The side effect says that if lem is added, then we should add the + // secant point c for (tf,d). + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + d_im.addPendingArithLemma(nlem, true); + } +} + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h new file mode 100644 index 000000000..2cf6400a3 --- /dev/null +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -0,0 +1,213 @@ +/********************* */ +/*! \file transcendental_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utilities for transcendental lemmas. + **/ + +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H + +#include "expr/node.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/taylor_generator.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +/** + * Holds common state and utilities for transcendental solvers. + * + * This includes common lookups and caches as well as generic utilities for + * secant plane lemmas and taylor approximations. + */ +struct TranscendentalState +{ + TranscendentalState(InferenceManager& im, NlModel& model); + + /** init last call + * + * This is called at the beginning of last call effort check, where + * assertions are the set of assertions belonging to arithmetic, + * false_asserts is the subset of assertions that are false in the current + * model, and xts is the set of extended function terms that are active in + * the current context. + * + * This call may add lemmas to lems based on registering term + * information (for example, purification of sine terms). + */ + void init(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); + + /** Initialize members for pi-related values */ + void mkPi(); + /** Get current bounds for pi as a lemma */ + void getCurrentPiBounds(); + + /** + * Get the two closest secant points from the once stored already. + * "closest" is determined according to the current model. + * @param e The transcendental term (like (exp t)) + * @param c The point currently under consideration (probably the model of t) + * @param d The taylor degree. + */ + std::pair getClosestSecantPoints(TNode e, TNode c, unsigned d); + + /** + * Construct a secant plane between b and c + * @param arg The argument of the transcendental term + * @param b Left secant point + * @param c Right secant point + * @param approx Approximation for b (not yet substituted) + * @param approx_c Approximation for c (already substituted) + */ + Node mkSecantPlane(TNode arg, TNode b, TNode c, TNode approx, TNode approx_c); + + /** + * Construct a secant lemma between lower and upper for tf. + * @param lower Left secant point + * @param upper Right secant point + * @param concavity Concavity of the current regions + * @param tf Current transcendental term + * @param splane Secant plane as computed by mkSecantPlane() + */ + NlLemma mkSecantLemma( + TNode lower, TNode upper, int concavity, TNode tf, TNode splane); + + /** + * Construct and send secant lemmas (if appropriate) + * @param bounds Secant bounds + * @param c Current point + * @param approx_c Approximation for c + * @param tf Current transcendental term + * @param d Current taylor degree + * @param concavity Concavity in region of c + */ + void doSecantLemmas(const std::pair& bounds, + TNode c, + TNode approx_c, + TNode tf, + unsigned d, + int concavity) + ; + + Node d_true; + Node d_false; + Node d_zero; + Node d_one; + Node d_neg_one; + + /** The inference manager that we push conflicts and lemmas to. */ + InferenceManager& d_im; + /** Reference to the non-linear model object */ + NlModel& d_model; + /** Utility to compute taylor approximations */ + TaylorGenerator d_taylor; + + /** + * 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 d_trMaster; + std::map> d_trSlaves; + + /** concavity region for transcendental functions + * + * This stores an integer that identifies an interval in + * which the current model value for an argument of an + * application of a transcendental function resides. + * + * For exp( x ): + * region #1 is -infty < x < infty + * For sin( x ): + * region #0 is pi < x < infty (this is an invalid region) + * region #1 is pi/2 < x <= pi + * region #2 is 0 < x <= pi/2 + * region #3 is -pi/2 < x <= 0 + * region #4 is -pi < x <= -pi/2 + * region #5 is -infty < x <= -pi (this is an invalid region) + * All regions not listed above, as well as regions 0 and 5 + * for SINE are "invalid". We only process applications + * of transcendental functions whose arguments have model + * values that reside in valid regions. + */ + std::unordered_map d_tf_region; + /** + * 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> d_funcCongClass; + /** + * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } + * that are representives of their congruence class. + */ + std::map> d_funcMap; + + /** secant points (sorted list) for transcendental functions + * + * This is used for tangent plane refinements for + * transcendental functions. This is the set + * "get-previous-secant-points" in "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017, for + * each transcendental function application. We store this set for each + * Taylor degree. + */ + std::unordered_map>, + NodeHashFunction> + d_secant_points; + + /** PI + * + * Note that PI is a (symbolic, non-constant) nullary operator. This is + * because its value cannot be computed exactly. We constraint PI to + * concrete lower and upper bounds stored in d_pi_bound below. + */ + Node d_pi; + /** PI/2 */ + Node d_pi_2; + /** -PI/2 */ + Node d_pi_neg_2; + /** -PI */ + Node d_pi_neg; + /** the concrete lower and upper bounds for PI */ + Node d_pi_bound[2]; + }; + +} // namespace transcendental +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory + +#endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */ diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp deleted file mode 100644 index 2e25f1642..000000000 --- a/src/theory/arith/nl/transcendental_solver.cpp +++ /dev/null @@ -1,1474 +0,0 @@ -/********************* */ -/*! \file transcendental_solver.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Gereon Kremer - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of solver for handling transcendental functions. - **/ - -#include "theory/arith/nl/transcendental_solver.h" - -#include -#include - -#include "expr/node_algorithm.h" -#include "expr/node_builder.h" -#include "options/arith_options.h" -#include "theory/arith/arith_msum.h" -#include "theory/arith/arith_utilities.h" -#include "theory/rewriter.h" - -using namespace CVC4::kind; - -namespace CVC4 { -namespace theory { -namespace arith { -namespace nl { - -TranscendentalSolver::TranscendentalSolver(InferenceManager& im, NlModel& m) : d_im(im), d_model(m) -{ - NodeManager* nm = NodeManager::currentNM(); - d_true = nm->mkConst(true); - d_false = nm->mkConst(false); - d_zero = nm->mkConst(Rational(0)); - d_one = nm->mkConst(Rational(1)); - d_neg_one = nm->mkConst(Rational(-1)); - d_taylor_real_fv = nm->mkBoundVar("x", nm->realType()); - d_taylor_real_fv_base = nm->mkBoundVar("a", nm->realType()); - d_taylor_real_fv_base_rem = nm->mkBoundVar("b", nm->realType()); - d_taylor_degree = options::nlExtTfTaylorDegree(); -} - -TranscendentalSolver::~TranscendentalSolver() {} - -void TranscendentalSolver::initLastCall(const std::vector& assertions, - const std::vector& false_asserts, - const std::vector& xts) -{ - d_funcCongClass.clear(); - d_funcMap.clear(); - d_tf_region.clear(); - - NodeManager* nm = NodeManager::currentNM(); - - // register the extended function terms - std::vector trNeedsMaster; - bool needPi = false; - // for computing congruence - std::map argTrie; - for (unsigned i = 0, xsize = xts.size(); i < xsize; i++) - { - Node a = xts[i]; - 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].insert(a); - } - } - } - if (ak == EXPONENTIAL || ak == SINE) - { - needPi = needPi || (ak == SINE); - // if we didn't indicate that it should be purified above - if (consider) - { - std::vector repList; - for (const Node& ac : a) - { - Node r = d_model.computeConcreteModelValue(ac); - repList.push_back(r); - } - Node aa = argTrie[ak].add(a, repList); - if (aa != a) - { - // apply congruence to pairs of terms that are disequal and congruent - Assert(aa.getNumChildren() == a.getNumChildren()); - Node mvaa = d_model.computeAbstractModelValue(a); - Node mvaaa = d_model.computeAbstractModelValue(aa); - if (mvaa != mvaaa) - { - std::vector exp; - for (unsigned j = 0, size = a.getNumChildren(); j < size; j++) - { - exp.push_back(a[j].eqNode(aa[j])); - } - Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); - Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa)); - d_im.addPendingArithLemma(cong_lemma, InferenceId::NL_CONGRUENCE); - } - } - else - { - // 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_funcMap[ak].push_back(a); - d_funcCongClass[a].push_back(a); - } - } - // initialize pi if necessary - if (needPi && d_pi.isNull()) - { - mkPi(); - getCurrentPiBounds(); - } - - if (d_im.hasUsed()) - { - return; - } - - // process SINE phase shifting - 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].insert(new_a); - d_trSlaves[new_a].insert(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 - { - // 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; - NlLemma nlem(lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG); - d_im.addPendingArithLemma(nlem); - } - - if (Trace.isOn("nl-ext-mv")) - { - Trace("nl-ext-mv") << "Arguments of trancendental functions : " - << std::endl; - for (std::pair >& tfl : d_funcMap) - { - Kind k = tfl.first; - if (k == SINE || k == EXPONENTIAL) - { - for (const Node& tf : tfl.second) - { - Node v = tf[0]; - d_model.computeConcreteModelValue(v); - d_model.computeAbstractModelValue(v); - d_model.printModelValue("nl-ext-mv", v); - } - } - } - } -} - -bool TranscendentalSolver::preprocessAssertionsCheckModel( - std::vector& assertions) -{ - std::vector pvars; - std::vector psubs; - for (const std::pair& tb : d_trMaster) - { - pvars.push_back(tb.first); - psubs.push_back(tb.second); - } - - // initialize representation of assertions - std::vector passertions; - for (const Node& a : assertions) - - { - Node pa = a; - if (!pvars.empty()) - { - pa = arithSubstitute(pa, pvars, psubs); - pa = Rewriter::rewrite(pa); - } - if (!pa.isConst() || !pa.getConst()) - { - Trace("nl-ext-cm-assert") << "- assert : " << pa << std::endl; - passertions.push_back(pa); - } - } - // get model bounds for all transcendental functions - Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..." - << std::endl; - for (std::pair >& 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 bl; - Node bu; - if (k == PI) - { - bl = d_pi_bound[0]; - bu = d_pi_bound[1]; - } - else - { - std::pair bounds = getTfModelBounds(tf, d_taylor_degree); - bl = bounds.first; - bu = bounds.second; - if (bl != bu) - { - d_model.setUsedApproximate(); - } - } - if (!bl.isNull() && !bu.isNull()) - { - // for each function in the congruence classe - for (const Node& ctf : d_funcCongClass[tf]) - { - // 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]) - { - Trace("nl-ext-cm") << "...bound for " << stf << " : [" << bl << ", " - << bu << "]" << std::endl; - success = d_model.addCheckModelBound(stf, bl, bu); - } - } - } - else - { - Trace("nl-ext-cm") << "...no bound for " << tf << std::endl; - } - if (!success) - { - // a bound was conflicting - Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl; - Trace("nl-ext-cm") << "-----" << std::endl; - return false; - } - } - } - // replace the assertions - assertions = passertions; - return true; -} - -void TranscendentalSolver::incrementTaylorDegree() { d_taylor_degree++; } -unsigned TranscendentalSolver::getTaylorDegree() const -{ - return d_taylor_degree; -} - -void TranscendentalSolver::processSideEffect(const NlLemma& se) -{ - for (const std::tuple& sp : se.d_secantPoint) - { - Node tf = std::get<0>(sp); - unsigned d = std::get<1>(sp); - Node c = std::get<2>(sp); - d_secant_points[tf][d].push_back(c); - } -} - -void TranscendentalSolver::mkPi() -{ - NodeManager* nm = NodeManager::currentNM(); - if (d_pi.isNull()) - { - d_pi = nm->mkNullaryOperator(nm->realType(), PI); - d_pi_2 = Rewriter::rewrite( - nm->mkNode(MULT, d_pi, nm->mkConst(Rational(1) / Rational(2)))); - d_pi_neg_2 = Rewriter::rewrite( - nm->mkNode(MULT, d_pi, nm->mkConst(Rational(-1) / Rational(2)))); - d_pi_neg = - Rewriter::rewrite(nm->mkNode(MULT, d_pi, nm->mkConst(Rational(-1)))); - // initialize bounds - d_pi_bound[0] = nm->mkConst(Rational(103993) / Rational(33102)); - d_pi_bound[1] = nm->mkConst(Rational(104348) / Rational(33215)); - } -} - -void TranscendentalSolver::getCurrentPiBounds() -{ - NodeManager* nm = NodeManager::currentNM(); - Node pi_lem = nm->mkNode(AND, - nm->mkNode(GEQ, d_pi, d_pi_bound[0]), - nm->mkNode(LEQ, d_pi, d_pi_bound[1])); - d_im.addPendingArithLemma(pi_lem, InferenceId::NL_T_PI_BOUND); -} - -void TranscendentalSolver::checkTranscendentalInitialRefine() -{ - NodeManager* nm = NodeManager::currentNM(); - Trace("nl-ext") - << "Get initial refinement lemmas for transcendental functions..." - << std::endl; - for (std::pair >& tfl : d_funcMap) - { - Kind k = tfl.first; - for (const Node& t : tfl.second) - { - // initial refinements - if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end()) - { - d_tf_initial_refine[t] = true; - Node lem; - if (k == SINE) - { - Node symn = nm->mkNode(SINE, nm->mkNode(MULT, d_neg_one, t[0])); - symn = Rewriter::rewrite(symn); - // 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].insert(symn); - Assert(d_trSlaves.find(t) != d_trSlaves.end()); - std::vector children; - - lem = nm->mkNode(AND, - // bounds - nm->mkNode(AND, - nm->mkNode(LEQ, t, d_one), - nm->mkNode(GEQ, t, d_neg_one)), - // symmetry - nm->mkNode(PLUS, t, symn).eqNode(d_zero), - // sign - nm->mkNode(EQUAL, - nm->mkNode(LT, t[0], d_zero), - nm->mkNode(LT, t, d_zero)), - // zero val - nm->mkNode(EQUAL, - nm->mkNode(GT, t[0], d_zero), - nm->mkNode(GT, t, d_zero))); - lem = nm->mkNode( - AND, - lem, - // zero tangent - nm->mkNode(AND, - nm->mkNode(IMPLIES, - nm->mkNode(GT, t[0], d_zero), - nm->mkNode(LT, t, t[0])), - nm->mkNode(IMPLIES, - nm->mkNode(LT, t[0], d_zero), - nm->mkNode(GT, t, t[0]))), - // pi tangent - nm->mkNode( - AND, - nm->mkNode(IMPLIES, - nm->mkNode(LT, t[0], d_pi), - nm->mkNode(LT, t, nm->mkNode(MINUS, d_pi, t[0]))), - nm->mkNode( - IMPLIES, - nm->mkNode(GT, t[0], d_pi_neg), - nm->mkNode(GT, t, nm->mkNode(MINUS, d_pi_neg, t[0]))))); - } - else if (k == EXPONENTIAL) - { - // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) < - // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 ) - lem = nm->mkNode( - AND, - nm->mkNode(GT, t, d_zero), - nm->mkNode(EQUAL, t[0].eqNode(d_zero), t.eqNode(d_one)), - nm->mkNode(EQUAL, - nm->mkNode(LT, t[0], d_zero), - nm->mkNode(LT, t, d_one)), - nm->mkNode(OR, - nm->mkNode(LEQ, t[0], d_zero), - nm->mkNode(GT, t, nm->mkNode(PLUS, t[0], d_one)))); - } - if (!lem.isNull()) - { - d_im.addPendingArithLemma(lem, InferenceId::NL_T_INIT_REFINE); - } - } - } - } -} - -void TranscendentalSolver::checkTranscendentalMonotonic() -{ - Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..." - << std::endl; - - // sort arguments of all transcendentals - std::map > sorted_tf_args; - std::map > tf_arg_to_term; - - for (std::pair >& tfl : d_funcMap) - { - Kind k = tfl.first; - if (k == EXPONENTIAL || k == SINE) - { - for (const Node& tf : tfl.second) - { - Node a = tf[0]; - Node mvaa = d_model.computeAbstractModelValue(a); - if (mvaa.isConst()) - { - Trace("nl-ext-tf-mono-debug") << "...tf term : " << a << std::endl; - sorted_tf_args[k].push_back(a); - tf_arg_to_term[k][a] = tf; - } - } - } - } - - SortNlModel smv; - smv.d_nlm = &d_model; - // sort by concrete values - smv.d_isConcrete = true; - smv.d_reverse_order = true; - for (std::pair >& tfl : d_funcMap) - { - Kind k = tfl.first; - if (!sorted_tf_args[k].empty()) - { - std::sort(sorted_tf_args[k].begin(), sorted_tf_args[k].end(), smv); - Trace("nl-ext-tf-mono") << "Sorted transcendental function list for " << k - << " : " << std::endl; - for (unsigned i = 0; i < sorted_tf_args[k].size(); i++) - { - Node targ = sorted_tf_args[k][i]; - Node mvatarg = d_model.computeAbstractModelValue(targ); - Trace("nl-ext-tf-mono") - << " " << targ << " -> " << mvatarg << std::endl; - Node t = tf_arg_to_term[k][targ]; - Node mvat = d_model.computeAbstractModelValue(t); - Trace("nl-ext-tf-mono") << " f-val : " << mvat << std::endl; - } - std::vector mpoints; - std::vector mpoints_vals; - if (k == SINE) - { - mpoints.push_back(d_pi); - mpoints.push_back(d_pi_2); - mpoints.push_back(d_zero); - mpoints.push_back(d_pi_neg_2); - mpoints.push_back(d_pi_neg); - } - else if (k == EXPONENTIAL) - { - mpoints.push_back(Node::null()); - } - if (!mpoints.empty()) - { - // get model values for points - for (unsigned i = 0; i < mpoints.size(); i++) - { - Node mpv; - if (!mpoints[i].isNull()) - { - mpv = d_model.computeAbstractModelValue(mpoints[i]); - Assert(mpv.isConst()); - } - mpoints_vals.push_back(mpv); - } - - unsigned mdir_index = 0; - int monotonic_dir = -1; - Node mono_bounds[2]; - Node targ, targval, t, tval; - for (unsigned i = 0, size = sorted_tf_args[k].size(); i < size; i++) - { - Node sarg = sorted_tf_args[k][i]; - Node sargval = d_model.computeAbstractModelValue(sarg); - Assert(sargval.isConst()); - Node s = tf_arg_to_term[k][sarg]; - Node sval = d_model.computeAbstractModelValue(s); - Assert(sval.isConst()); - - // increment to the proper monotonicity region - bool increment = true; - while (increment && mdir_index < mpoints.size()) - { - increment = false; - if (mpoints[mdir_index].isNull()) - { - increment = true; - } - else - { - Node pval = mpoints_vals[mdir_index]; - Assert(pval.isConst()); - if (sargval.getConst() < pval.getConst()) - { - increment = true; - Trace("nl-ext-tf-mono") << "...increment at " << sarg - << " since model value is less than " - << mpoints[mdir_index] << std::endl; - } - } - if (increment) - { - tval = Node::null(); - mono_bounds[1] = mpoints[mdir_index]; - mdir_index++; - monotonic_dir = regionToMonotonicityDir(k, mdir_index); - if (mdir_index < mpoints.size()) - { - mono_bounds[0] = mpoints[mdir_index]; - } - else - { - mono_bounds[0] = Node::null(); - } - } - } - // store the concavity region - d_tf_region[s] = mdir_index; - Trace("nl-ext-concavity") << "Transcendental function " << s - << " is in region #" << mdir_index; - Trace("nl-ext-concavity") - << ", arg model value = " << sargval << std::endl; - - if (!tval.isNull()) - { - NodeManager* nm = NodeManager::currentNM(); - Node mono_lem; - if (monotonic_dir == 1 - && sval.getConst() > tval.getConst()) - { - mono_lem = nm->mkNode( - IMPLIES, nm->mkNode(GEQ, targ, sarg), nm->mkNode(GEQ, t, s)); - } - else if (monotonic_dir == -1 - && sval.getConst() < tval.getConst()) - { - mono_lem = nm->mkNode( - IMPLIES, nm->mkNode(LEQ, targ, sarg), nm->mkNode(LEQ, t, s)); - } - if (!mono_lem.isNull()) - { - if (!mono_bounds[0].isNull()) - { - Assert(!mono_bounds[1].isNull()); - mono_lem = nm->mkNode( - IMPLIES, - nm->mkNode(AND, - mkBounded(mono_bounds[0], targ, mono_bounds[1]), - mkBounded(mono_bounds[0], sarg, mono_bounds[1])), - mono_lem); - } - Trace("nl-ext-tf-mono") - << "Monotonicity lemma : " << mono_lem << std::endl; - - d_im.addPendingArithLemma(mono_lem, InferenceId::NL_T_MONOTONICITY); - } - } - // store the previous values - targ = sarg; - targval = sargval; - t = s; - tval = sval; - } - } - } - } -} - -void TranscendentalSolver::checkTranscendentalTangentPlanes() -{ - Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..." - << std::endl; - // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions - // via Incremental Linearization" by Cimatti et al - for (std::pair >& tfs : d_funcMap) - { - Kind k = tfs.first; - if (k == PI) - { - // We do not use Taylor approximation for PI currently. - // This is because the convergence is extremely slow, and hence an - // initial approximation is superior. - continue; - } - Trace("nl-ext-tftp-debug2") << "Taylor variables: " << std::endl; - Trace("nl-ext-tftp-debug2") - << " taylor_real_fv : " << d_taylor_real_fv << std::endl; - Trace("nl-ext-tftp-debug2") - << " taylor_real_fv_base : " << d_taylor_real_fv_base << std::endl; - Trace("nl-ext-tftp-debug2") - << " taylor_real_fv_base_rem : " << d_taylor_real_fv_base_rem - << std::endl; - Trace("nl-ext-tftp-debug2") << std::endl; - - // we substitute into the Taylor sum P_{n,f(0)}( x ) - - for (const Node& tf : tfs.second) - { - // tf is Figure 3 : tf( x ) - 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 = d_im.numPendingLemmas() + d_im.numWaitingLemmas(); - if (checkTfTangentPlanesFun(tf, d)) - { - Trace("nl-ext-tftp") - << "...fail, #lemmas = " - << (d_im.numPendingLemmas() + d_im.numWaitingLemmas() - prev) - << std::endl; - break; - } - else - { - Trace("nl-ext-tftp") << "...success" << std::endl; - } - } - } - } -} - -bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, - unsigned d) -{ - 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().sgn(); - if (csign == 0) - { - // no secant/tangent plane is necessary - return true; - } - Assert(csign == 1 || csign == -1); - - // Figure 3: P_l, P_u - // mapped to for signs of c - std::map poly_approx_bounds[2]; - std::vector pbounds; - getPolynomialApproximationBoundForArg(k, c, d, pbounds); - poly_approx_bounds[0][1] = pbounds[0]; - poly_approx_bounds[0][-1] = pbounds[1]; - poly_approx_bounds[1][1] = pbounds[2]; - poly_approx_bounds[1][-1] = pbounds[3]; - - // Figure 3 : v - Node v = d_model.computeAbstractModelValue(tf); - - // check value of tf - Trace("nl-ext-tftp-debug") << "Process tangent plane refinement for " << tf - << ", degree " << d << "..." << std::endl; - Trace("nl-ext-tftp-debug") << " value in model : " << v << std::endl; - Trace("nl-ext-tftp-debug") << " arg value in model : " << c << std::endl; - - std::vector taylor_vars; - taylor_vars.push_back(d_taylor_real_fv); - - // compute the concavity - int region = -1; - std::unordered_map::iterator itr = - d_tf_region.find(tf); - if (itr != d_tf_region.end()) - { - region = itr->second; - Trace("nl-ext-tftp-debug") << " region is : " << region << std::endl; - } - // Figure 3 : conc - int concavity = regionToConcavity(k, itr->second); - Trace("nl-ext-tftp-debug") << " concavity is : " << concavity << std::endl; - if (concavity == 0) - { - // no secant/tangent plane is necessary - return true; - } - // bounds for which we are this concavity - // Figure 3: < l, u > - Node bounds[2]; - if (k == SINE) - { - bounds[0] = regionToLowerBound(k, region); - Assert(!bounds[0].isNull()); - bounds[1] = regionToUpperBound(k, region); - Assert(!bounds[1].isNull()); - } - - // Figure 3: P - Node poly_approx; - - // compute whether this is a tangent refinement or a secant refinement - bool is_tangent = false; - bool is_secant = false; - std::pair mvb = getTfModelBounds(tf, d); - // this is the approximated value of tf(c), which is a value such that: - // M_A(tf(c)) >= poly_appox_c >= tf(c) or - // M_A(tf(c)) <= poly_appox_c <= tf(c) - // In other words, it is a better approximation of the true value of tf(c) - // in the case that we add a refinement lemma. We use this value in the - // refinement schemas below. - Node poly_approx_c; - for (unsigned r = 0; r < 2; r++) - { - Node pab = poly_approx_bounds[r][csign]; - Node v_pab = r == 0 ? mvb.first : mvb.second; - if (!v_pab.isNull()) - { - Trace("nl-ext-tftp-debug2") - << "...model value of " << pab << " is " << v_pab << std::endl; - - Assert(v_pab.isConst()); - Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab); - Trace("nl-ext-tftp-debug2") << "...compare : " << comp << std::endl; - Node compr = Rewriter::rewrite(comp); - Trace("nl-ext-tftp-debug2") << "...got : " << compr << std::endl; - if (compr == d_true) - { - poly_approx_c = v_pab; - // beyond the bounds - if (r == 0) - { - poly_approx = poly_approx_bounds[r][csign]; - is_tangent = concavity == 1; - is_secant = concavity == -1; - } - else - { - poly_approx = poly_approx_bounds[r][csign]; - is_tangent = concavity == -1; - is_secant = concavity == 1; - } - if (Trace.isOn("nl-ext-tftp")) - { - Trace("nl-ext-tftp") << "*** Outside boundary point ("; - Trace("nl-ext-tftp") << (r == 0 ? "low" : "high") << ") "; - printRationalApprox("nl-ext-tftp", v_pab); - Trace("nl-ext-tftp") << ", will refine..." << std::endl; - Trace("nl-ext-tftp") - << " poly_approx = " << poly_approx << std::endl; - Trace("nl-ext-tftp") - << " is_tangent = " << is_tangent << std::endl; - Trace("nl-ext-tftp") << " is_secant = " << is_secant << std::endl; - } - break; - } - else - { - Trace("nl-ext-tftp") - << " ...within " << (r == 0 ? "low" : "high") << " bound : "; - printRationalApprox("nl-ext-tftp", v_pab); - Trace("nl-ext-tftp") << std::endl; - } - } - } - - // Figure 3: P( c ) - if (is_tangent || is_secant) - { - Trace("nl-ext-tftp-debug2") - << "...poly approximation at c is " << poly_approx_c << std::endl; - } - else - { - // we may want to continue getting better bounds - return false; - } - - if (is_tangent) - { - // compute tangent plane - // Figure 3: T( x ) - // We use zero slope tangent planes, since the concavity of the Taylor - // approximation cannot be easily established. - Node tplane = poly_approx_c; - - Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane); - std::vector antec; - int mdir = regionToMonotonicityDir(k, region); - for (unsigned i = 0; i < 2; i++) - { - // Tangent plane is valid in the interval [c,u) if the slope of the - // function matches its concavity, and is valid in (l, c] otherwise. - Node use_bound = (mdir == concavity) == (i == 0) ? c : bounds[i]; - if (!use_bound.isNull()) - { - Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], use_bound); - antec.push_back(ant); - } - } - if (!antec.empty()) - { - Node antec_n = antec.size() == 1 ? antec[0] : nm->mkNode(AND, antec); - lem = nm->mkNode(IMPLIES, antec_n, lem); - } - Trace("nl-ext-tftp-debug2") - << "*** Tangent plane lemma (pre-rewrite): " << lem << std::endl; - lem = Rewriter::rewrite(lem); - Trace("nl-ext-tftp-lemma") - << "*** Tangent plane lemma : " << lem << std::endl; - Assert(d_model.computeAbstractModelValue(lem) == d_false); - // Figure 3 : line 9 - d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); - } - else if (is_secant) - { - // bounds are the minimum and maximum previous secant points - // should not repeat secant points: secant lemmas should suffice to - // rule out previous assignment - Assert(std::find( - d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c) - == d_secant_points[tf][d].end()); - // Insert into the (temporary) vector. We do not update this vector - // until we are sure this secant plane lemma has been processed. We do - // this by mapping the lemma to a side effect below. - std::vector spoints = d_secant_points[tf][d]; - spoints.push_back(c); - - // sort - SortNlModel smv; - smv.d_nlm = &d_model; - smv.d_isConcrete = true; - std::sort(spoints.begin(), spoints.end(), smv); - // get the resulting index of c - unsigned index = - std::find(spoints.begin(), spoints.end(), c) - spoints.begin(); - // bounds are the next closest upper/lower bound values - if (index > 0) - { - bounds[0] = spoints[index - 1]; - } - else - { - // otherwise, we use the lower boundary point for this concavity - // region - if (k == SINE) - { - Assert(!bounds[0].isNull()); - } - else if (k == EXPONENTIAL) - { - // pick c-1 - bounds[0] = Rewriter::rewrite(nm->mkNode(MINUS, c, d_one)); - } - } - if (index < spoints.size() - 1) - { - bounds[1] = spoints[index + 1]; - } - else - { - // otherwise, we use the upper boundary point for this concavity - // region - if (k == SINE) - { - Assert(!bounds[1].isNull()); - } - else if (k == EXPONENTIAL) - { - // pick c+1 - bounds[1] = Rewriter::rewrite(nm->mkNode(PLUS, c, d_one)); - } - } - Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds[0] - << " ... " << bounds[1] << std::endl; - - // the secant plane may be conjunction of 1-2 guarded inequalities - std::vector lemmaConj; - for (unsigned s = 0; s < 2; s++) - { - // compute secant plane - Assert(!poly_approx.isNull()); - Assert(!bounds[s].isNull()); - // take the model value of l or u (since may contain PI) - Node b = d_model.computeAbstractModelValue(bounds[s]); - Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds[s] - << " is " << b << std::endl; - Assert(b.isConst()); - if (c != b) - { - // Figure 3 : P(l), P(u), for s = 0,1 - Node poly_approx_b; - std::vector taylor_subs; - taylor_subs.push_back(b); - Assert(taylor_vars.size() == taylor_subs.size()); - poly_approx_b = poly_approx.substitute(taylor_vars.begin(), - taylor_vars.end(), - taylor_subs.begin(), - taylor_subs.end()); - // Figure 3: S_l( x ), S_u( x ) for s = 0,1 - Node splane; - Node rcoeff_n = Rewriter::rewrite(nm->mkNode(MINUS, b, c)); - Assert(rcoeff_n.isConst()); - Rational rcoeff = rcoeff_n.getConst(); - Assert(rcoeff.sgn() != 0); - poly_approx_b = Rewriter::rewrite(poly_approx_b); - poly_approx_c = Rewriter::rewrite(poly_approx_c); - splane = nm->mkNode( - PLUS, - poly_approx_b, - nm->mkNode(MULT, - nm->mkNode(MINUS, poly_approx_b, poly_approx_c), - nm->mkConst(Rational(1) / rcoeff), - nm->mkNode(MINUS, tf[0], b))); - - Node lem = nm->mkNode(concavity == 1 ? LEQ : GEQ, tf, splane); - // With respect to Figure 3, this is slightly different. - // In particular, we chose b to be the model value of bounds[s], - // which is a constant although bounds[s] may not be (e.g. if it - // contains PI). - // To ensure that c...b does not cross an inflection point, - // we guard with the symbolic version of bounds[s]. - // This leads to lemmas e.g. of this form: - // ( c <= x <= PI/2 ) => ( sin(x) < ( P( b ) - P( c ) )*( x - - // b ) + P( b ) ) - // where b = (PI/2)^M, the current value of PI/2 in the model. - // This is sound since we are guarded by the symbolic - // representation of PI/2. - Node antec_n = - nm->mkNode(AND, - nm->mkNode(GEQ, tf[0], s == 0 ? bounds[s] : c), - nm->mkNode(LEQ, tf[0], s == 0 ? c : bounds[s])); - lem = nm->mkNode(IMPLIES, antec_n, lem); - Trace("nl-ext-tftp-debug2") - << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl; - lem = Rewriter::rewrite(lem); - Trace("nl-ext-tftp-lemma") - << "*** Secant plane lemma : " << lem << std::endl; - lemmaConj.push_back(lem); - Assert(d_model.computeAbstractModelValue(lem) == d_false); - } - } - // Figure 3 : line 22 - Assert(!lemmaConj.empty()); - Node lem = - lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj); - NlLemma nlem(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT); - // The side effect says that if lem is added, then we should add the - // secant point c for (tf,d). - nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); - d_im.addPendingArithLemma(nlem, true); - } - return true; -} - -int TranscendentalSolver::regionToMonotonicityDir(Kind k, int region) -{ - if (k == EXPONENTIAL) - { - if (region == 1) - { - return 1; - } - } - else if (k == SINE) - { - if (region == 1 || region == 4) - { - return -1; - } - else if (region == 2 || region == 3) - { - return 1; - } - } - return 0; -} - -int TranscendentalSolver::regionToConcavity(Kind k, int region) -{ - if (k == EXPONENTIAL) - { - if (region == 1) - { - return 1; - } - } - else if (k == SINE) - { - if (region == 1 || region == 2) - { - return -1; - } - else if (region == 3 || region == 4) - { - return 1; - } - } - return 0; -} - -Node TranscendentalSolver::regionToLowerBound(Kind k, int region) -{ - if (k == SINE) - { - if (region == 1) - { - return d_pi_2; - } - else if (region == 2) - { - return d_zero; - } - else if (region == 3) - { - return d_pi_neg_2; - } - else if (region == 4) - { - return d_pi_neg; - } - } - return Node::null(); -} - -Node TranscendentalSolver::regionToUpperBound(Kind k, int region) -{ - if (k == SINE) - { - if (region == 1) - { - return d_pi; - } - else if (region == 2) - { - return d_pi_2; - } - else if (region == 3) - { - return d_zero; - } - else if (region == 4) - { - return d_pi_neg_2; - } - } - return Node::null(); -} - -Node TranscendentalSolver::getDerivative(Node n, Node x) -{ - NodeManager* nm = NodeManager::currentNM(); - Assert(x.isVar()); - // only handle the cases of the taylor expansion of d - if (n.getKind() == EXPONENTIAL) - { - if (n[0] == x) - { - return n; - } - } - else if (n.getKind() == SINE) - { - if (n[0] == x) - { - Node na = nm->mkNode(MINUS, d_pi_2, n[0]); - Node ret = nm->mkNode(SINE, na); - ret = Rewriter::rewrite(ret); - return ret; - } - } - else if (n.getKind() == PLUS) - { - std::vector dchildren; - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - // PLUS is flattened in rewriter, recursion depth is bounded by 1 - Node dc = getDerivative(n[i], x); - if (dc.isNull()) - { - return dc; - } - else - { - dchildren.push_back(dc); - } - } - return nm->mkNode(PLUS, dchildren); - } - else if (n.getKind() == MULT) - { - Assert(n[0].isConst()); - Node dc = getDerivative(n[1], x); - if (!dc.isNull()) - { - return nm->mkNode(MULT, n[0], dc); - } - } - else if (n.getKind() == NONLINEAR_MULT) - { - unsigned xcount = 0; - std::vector children; - unsigned xindex = 0; - for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) - { - if (n[i] == x) - { - xcount++; - xindex = i; - } - children.push_back(n[i]); - } - if (xcount == 0) - { - return d_zero; - } - else - { - children[xindex] = nm->mkConst(Rational(xcount)); - } - return nm->mkNode(MULT, children); - } - else if (n.isVar()) - { - return n == x ? d_one : d_zero; - } - else if (n.isConst()) - { - return d_zero; - } - Trace("nl-ext-debug") << "No derivative computed for " << n; - Trace("nl-ext-debug") << " for d/d{" << x << "}" << std::endl; - return Node::null(); -} - -std::pair TranscendentalSolver::getTaylor(Node fa, unsigned n) -{ - NodeManager* nm = NodeManager::currentNM(); - Assert(n > 0); - Node fac; // what term we cache for fa - if (fa[0] == d_zero) - { - // optimization : simpler to compute (x-fa[0])^n if we are centered around 0 - fac = fa; - } - else - { - // otherwise we use a standard factor a in (x-a)^n - fac = nm->mkNode(fa.getKind(), d_taylor_real_fv_base); - } - Node taylor_rem; - Node taylor_sum; - // check if we have already computed this Taylor series - std::unordered_map::iterator itt = d_taylor_sum[fac].find(n); - if (itt == d_taylor_sum[fac].end()) - { - Node i_exp_base; - if (fa[0] == d_zero) - { - i_exp_base = d_taylor_real_fv; - } - else - { - i_exp_base = Rewriter::rewrite( - nm->mkNode(MINUS, d_taylor_real_fv, d_taylor_real_fv_base)); - } - Node i_derv = fac; - Node i_fact = d_one; - Node i_exp = d_one; - int i_derv_status = 0; - unsigned counter = 0; - std::vector sum; - do - { - counter++; - if (fa.getKind() == EXPONENTIAL) - { - // unchanged - } - else if (fa.getKind() == SINE) - { - if (i_derv_status % 2 == 1) - { - Node arg = nm->mkNode(PLUS, d_pi_2, d_taylor_real_fv_base); - i_derv = nm->mkNode(SINE, arg); - } - else - { - i_derv = fa; - } - if (i_derv_status >= 2) - { - i_derv = nm->mkNode(MINUS, d_zero, i_derv); - } - i_derv = Rewriter::rewrite(i_derv); - i_derv_status = i_derv_status == 3 ? 0 : i_derv_status + 1; - } - if (counter == (n + 1)) - { - TNode x = d_taylor_real_fv_base; - i_derv = i_derv.substitute(x, d_taylor_real_fv_base_rem); - } - Node curr = nm->mkNode(MULT, nm->mkNode(DIVISION, i_derv, i_fact), i_exp); - if (counter == (n + 1)) - { - taylor_rem = curr; - } - else - { - sum.push_back(curr); - i_fact = Rewriter::rewrite( - nm->mkNode(MULT, nm->mkConst(Rational(counter)), i_fact)); - i_exp = Rewriter::rewrite(nm->mkNode(MULT, i_exp_base, i_exp)); - } - } while (counter <= n); - taylor_sum = sum.size() == 1 ? sum[0] : nm->mkNode(PLUS, sum); - - if (fac[0] != d_taylor_real_fv_base) - { - TNode x = d_taylor_real_fv_base; - taylor_sum = taylor_sum.substitute(x, fac[0]); - } - - // cache - d_taylor_sum[fac][n] = taylor_sum; - d_taylor_rem[fac][n] = taylor_rem; - } - else - { - taylor_sum = itt->second; - Assert(d_taylor_rem[fac].find(n) != d_taylor_rem[fac].end()); - taylor_rem = d_taylor_rem[fac][n]; - } - - // must substitute for the argument if we were using a different lookup - if (fa[0] != fac[0]) - { - TNode x = d_taylor_real_fv_base; - taylor_sum = taylor_sum.substitute(x, fa[0]); - } - return std::pair(taylor_sum, taylor_rem); -} - -void TranscendentalSolver::getPolynomialApproximationBounds( - Kind k, unsigned d, std::vector& pbounds) -{ - if (d_poly_bounds[k][d].empty()) - { - NodeManager* nm = NodeManager::currentNM(); - Node tft = nm->mkNode(k, d_zero); - // n is the Taylor degree we are currently considering - unsigned n = 2 * d; - // n must be even - std::pair taylor = getTaylor(tft, n); - Trace("nl-ext-tftp-debug2") - << "Taylor for " << k << " is : " << taylor.first << std::endl; - Node taylor_sum = Rewriter::rewrite(taylor.first); - Trace("nl-ext-tftp-debug2") - << "Taylor for " << k << " is (post-rewrite) : " << taylor_sum - << std::endl; - Assert(taylor.second.getKind() == MULT); - Assert(taylor.second.getNumChildren() == 2); - Assert(taylor.second[0].getKind() == DIVISION); - Trace("nl-ext-tftp-debug2") - << "Taylor remainder for " << k << " is " << taylor.second << std::endl; - // ru is x^{n+1}/(n+1)! - Node ru = nm->mkNode(DIVISION, taylor.second[1], taylor.second[0][1]); - ru = Rewriter::rewrite(ru); - Trace("nl-ext-tftp-debug2") - << "Taylor remainder factor is (post-rewrite) : " << ru << std::endl; - if (k == EXPONENTIAL) - { - pbounds.push_back(taylor_sum); - pbounds.push_back(taylor_sum); - pbounds.push_back(Rewriter::rewrite( - nm->mkNode(MULT, taylor_sum, nm->mkNode(PLUS, d_one, ru)))); - pbounds.push_back(Rewriter::rewrite(nm->mkNode(PLUS, taylor_sum, ru))); - } - else - { - Assert(k == SINE); - Node l = Rewriter::rewrite(nm->mkNode(MINUS, taylor_sum, ru)); - Node u = Rewriter::rewrite(nm->mkNode(PLUS, taylor_sum, ru)); - pbounds.push_back(l); - pbounds.push_back(l); - pbounds.push_back(u); - pbounds.push_back(u); - } - Trace("nl-ext-tf-tplanes") - << "Polynomial approximation for " << k << " is: " << std::endl; - Trace("nl-ext-tf-tplanes") << " Lower (pos): " << pbounds[0] << std::endl; - Trace("nl-ext-tf-tplanes") << " Upper (pos): " << pbounds[2] << std::endl; - Trace("nl-ext-tf-tplanes") << " Lower (neg): " << pbounds[1] << std::endl; - Trace("nl-ext-tf-tplanes") << " Upper (neg): " << pbounds[3] << std::endl; - d_poly_bounds[k][d].insert( - d_poly_bounds[k][d].end(), pbounds.begin(), pbounds.end()); - } - else - { - pbounds.insert( - pbounds.end(), d_poly_bounds[k][d].begin(), d_poly_bounds[k][d].end()); - } -} - -void TranscendentalSolver::getPolynomialApproximationBoundForArg( - Kind k, Node c, unsigned d, std::vector& pbounds) -{ - getPolynomialApproximationBounds(k, d, pbounds); - Assert(c.isConst()); - if (k == EXPONENTIAL && c.getConst().sgn() == 1) - { - NodeManager* nm = NodeManager::currentNM(); - Node tft = nm->mkNode(k, d_zero); - bool success = false; - unsigned ds = d; - TNode ttrf = d_taylor_real_fv; - TNode tc = c; - do - { - success = true; - unsigned n = 2 * ds; - std::pair taylor = getTaylor(tft, n); - // check that 1-c^{n+1}/(n+1)! > 0 - Node ru = nm->mkNode(DIVISION, taylor.second[1], taylor.second[0][1]); - Node rus = ru.substitute(ttrf, tc); - rus = Rewriter::rewrite(rus); - Assert(rus.isConst()); - if (rus.getConst() > d_one.getConst()) - { - success = false; - ds = ds + 1; - } - } while (!success); - if (ds > d) - { - Trace("nl-ext-exp-taylor") - << "*** Increase Taylor bound to " << ds << " > " << d << " for (" - << k << " " << c << ")" << std::endl; - // must use sound upper bound - std::vector pboundss; - getPolynomialApproximationBounds(k, ds, pboundss); - pbounds[2] = pboundss[2]; - } - } -} - -std::pair TranscendentalSolver::getTfModelBounds(Node tf, - unsigned d) -{ - // compute the model value of the argument - Node c = d_model.computeAbstractModelValue(tf[0]); - Assert(c.isConst()); - int csign = c.getConst().sgn(); - Kind k = tf.getKind(); - if (csign == 0) - { - // at zero, its trivial - if (k == SINE) - { - return std::pair(d_zero, d_zero); - } - Assert(k == EXPONENTIAL); - return std::pair(d_one, d_one); - } - bool isNeg = csign == -1; - - std::vector pbounds; - getPolynomialApproximationBoundForArg(k, c, d, pbounds); - - std::vector bounds; - TNode tfv = d_taylor_real_fv; - TNode tfs = tf[0]; - for (unsigned d2 = 0; d2 < 2; d2++) - { - int index = d2 == 0 ? (isNeg ? 1 : 0) : (isNeg ? 3 : 2); - Node pab = pbounds[index]; - if (!pab.isNull()) - { - // { x -> M_A(tf[0]) } - // Notice that we compute the model value of tfs first, so that - // the call to rewrite below does not modify the term, where notice that - // rewrite( x*x { x -> M_A(t) } ) = M_A(t)*M_A(t) - // is not equal to - // M_A( x*x { x -> t } ) = M_A( t*t ) - // where M_A denotes the abstract model. - Node mtfs = d_model.computeAbstractModelValue(tfs); - pab = pab.substitute(tfv, mtfs); - pab = Rewriter::rewrite(pab); - Assert (pab.isConst()); - bounds.push_back(pab); - } - else - { - bounds.push_back(Node::null()); - } - } - return std::pair(bounds[0], bounds[1]); -} - -Node TranscendentalSolver::mkValidPhase(Node a, Node pi) -{ - return mkBounded( - NodeManager::currentNM()->mkNode(MULT, mkRationalNode(-1), pi), a, pi); -} - -} // namespace nl -} // namespace arith -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental_solver.h b/src/theory/arith/nl/transcendental_solver.h deleted file mode 100644 index 004221be2..000000000 --- a/src/theory/arith/nl/transcendental_solver.h +++ /dev/null @@ -1,423 +0,0 @@ -/********************* */ -/*! \file transcendental_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Solving for handling transcendental functions. - **/ - -#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL_SOLVER_H -#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL_SOLVER_H - -#include -#include -#include -#include - -#include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" - -namespace CVC4 { -namespace theory { -namespace arith { -namespace nl { - -/** Transcendental solver class - * - * This class implements model-based refinement schemes - * for transcendental functions, described in: - * - * - "Satisfiability Modulo Transcendental - * Functions via Incremental Linearization" by Cimatti - * et al., CADE 2017. - * - * It's main functionality are methods that implement lemma schemas below, - * which return a set of lemmas that should be sent on the output channel. - */ -class TranscendentalSolver -{ - public: - TranscendentalSolver(InferenceManager& im, NlModel& m); - ~TranscendentalSolver(); - - /** init last call - * - * This is called at the beginning of last call effort check, where - * assertions are the set of assertions belonging to arithmetic, - * false_asserts is the subset of assertions that are false in the current - * model, and xts is the set of extended function terms that are active in - * the current context. - * - * This call may add lemmas to lems based on registering term - * information (for example, purification of sine terms). - */ - void initLastCall(const std::vector& assertions, - const std::vector& false_asserts, - const std::vector& xts); - /** increment taylor degree */ - void incrementTaylorDegree(); - /** get taylor degree */ - unsigned getTaylorDegree() const; - /** preprocess assertions check model - * - * This modifies the given assertions in preparation for running a call - * to check model. - * - * This method returns false if a bound for a transcendental function - * was conflicting. - */ - bool preprocessAssertionsCheckModel(std::vector& assertions); - /** Process side effects in lemma se */ - void processSideEffect(const NlLemma& se); - //-------------------------------------------- lemma schemas - /** check transcendental initial refine - * - * Constructs a set of valid theory lemmas, based on - * simple facts about transcendental functions. - * This mostly follows the initial axioms described in - * Section 4 of "Satisfiability - * Modulo Transcendental Functions via Incremental - * Linearization" by Cimatti et al., CADE 2017. - * - * Examples: - * - * sin( x ) = -sin( -x ) - * ( PI > x > 0 ) => 0 < sin( x ) < 1 - * exp( x )>0 - * x<0 => exp( x )<1 - */ - void checkTranscendentalInitialRefine(); - - /** check transcendental monotonic - * - * Constructs a set of valid theory lemmas, based on a - * lemma scheme that ensures that applications - * of transcendental functions respect monotonicity. - * - * Examples: - * - * x > y => exp( x ) > exp( y ) - * PI/2 > x > y > 0 => sin( x ) > sin( y ) - * PI > x > y > PI/2 => sin( x ) < sin( y ) - */ - void checkTranscendentalMonotonic(); - - /** check transcendental tangent planes - * - * Constructs a set of valid theory lemmas, based on - * computing an "incremental linearization" of - * transcendental functions based on the model values - * of transcendental functions and their arguments. - * It is based on Figure 3 of "Satisfiability - * Modulo Transcendental Functions via Incremental - * Linearization" by Cimatti et al., CADE 2017. - * This schema is not terminating in general. - * It is not enabled by default, and can - * be enabled by --nl-ext-tf-tplanes. - * - * Example: - * - * Assume we have a term sin(y) where M( y ) = 1 where M is the current model. - * Note that: - * sin(1) ~= .841471 - * - * The Taylor series and remainder of sin(y) of degree 7 is - * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5 - * R_{7,sin(0),b}( x ) = (-1/5040)*x^7 - * - * This gives us lower and upper bounds : - * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x ) - * ...where note P_u( 1 ) = 4243/5040 ~= .841865 - * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x ) - * ...where note P_l( 1 ) = 4241/5040 ~= .841468 - * - * Assume that M( sin(y) ) > P_u( 1 ). - * Since the concavity of sine in the region 0 < x < PI/2 is -1, - * we add a tangent plane refinement. - * The tangent plane at the point 1 in P_u is - * given by the formula: - * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 ) - * We add the lemma: - * ( 0 < y < PI/2 ) => sin( y ) <= T( y ) - * which is: - * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506) - * - * Assume that M( sin(y) ) < P_u( 1 ). - * Since the concavity of sine in the region 0 < x < PI/2 is -1, - * we add a secant plane refinement for some constants ( l, u ) - * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose - * l = 0 and u = M( PI/2 ) = 150517/47912. - * The secant planes at point 1 for P_l - * are given by the formulas: - * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l ) - * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u ) - * We add the lemmas: - * ( 0 < y < 1 ) => sin( y ) >= S_l( y ) - * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y ) - * which are: - * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y - * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2) - * where c1, c2 are rationals (for brevity, omitted here) - * such that c1 ~= .277 and c2 ~= 2.032. - */ - void checkTranscendentalTangentPlanes(); - private: - /** check transcendental function refinement for tf - * - * 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, which includes the side effect of the lemma - * (if one exists). - * - * It returns false if the bounds are not precise enough to add a - * secant or tangent plane lemma. - */ - bool checkTfTangentPlanesFun(Node tf, unsigned d); - //-------------------------------------------- end lemma schemas - /** polynomial approximation bounds - * - * This adds P_l+[x], P_l-[x], P_u+[x], P_u-[x] to pbounds, where x is - * d_taylor_real_fv. These are polynomial approximations of the Taylor series - * of ( 0 ) for degree 2*d where k is SINE or EXPONENTIAL. - * These correspond to P_l and P_u from Figure 3 of Cimatti et al., CADE 2017, - * for positive/negative (+/-) values of the argument of ( 0 ). - * - * Notice that for certain bounds (e.g. upper bounds for exponential), the - * Taylor approximation for a fixed degree is only sound up to a given - * upper bound on the argument. To obtain sound lower/upper bounds for a - * given ( c ), use the function below. - */ - void getPolynomialApproximationBounds(Kind k, - unsigned d, - std::vector& pbounds); - /** polynomial approximation bounds - * - * This computes polynomial approximations P_l+[x], P_l-[x], P_u+[x], P_u-[x] - * that are sound (lower, upper) bounds for ( c ). Notice that these - * polynomials may depend on c. In particular, for P_u+[x] for ( c ) where - * c>0, we return the P_u+[x] from the function above for the minimum degree - * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive. - */ - void getPolynomialApproximationBoundForArg(Kind k, - Node c, - unsigned d, - std::vector& pbounds); - /** get transcendental function model bounds - * - * This returns the current lower and upper bounds of transcendental - * function application tf based on Taylor of degree 2*d, which is dependent - * on the model value of its argument. - */ - std::pair getTfModelBounds(Node tf, unsigned d); - /** get monotonicity direction - * - * Returns whether the slope is positive (+1) or negative(-1) - * in region of transcendental function with kind k. - * Returns 0 if region is invalid. - */ - int regionToMonotonicityDir(Kind k, int region); - /** get concavity - * - * Returns whether we are concave (+1) or convex (-1) - * in region of transcendental function with kind k, - * where region is defined above. - * Returns 0 if region is invalid. - */ - int regionToConcavity(Kind k, int region); - /** region to lower bound - * - * Returns the term corresponding to the lower - * bound of the region of transcendental function - * with kind k. Returns Node::null if the region - * is invalid, or there is no lower bound for the - * region. - */ - Node regionToLowerBound(Kind k, int region); - /** region to upper bound - * - * Returns the term corresponding to the upper - * bound of the region of transcendental function - * with kind k. Returns Node::null if the region - * is invalid, or there is no upper bound for the - * region. - */ - Node regionToUpperBound(Kind k, int region); - /** get derivative - * - * Returns d/dx n. Supports cases of n - * for transcendental functions applied to x, - * multiplication, addition, constants and variables. - * Returns Node::null() if derivative is an - * unhandled case. - */ - Node getDerivative(Node n, Node x); - - void mkPi(); - void getCurrentPiBounds(); - /** Make the node -pi <= a <= pi */ - static Node mkValidPhase(Node a, Node pi); - - /** The inference manager that we push conflicts and lemmas to. */ - InferenceManager& d_im; - /** Reference to the non-linear model object */ - NlModel& d_model; - /** commonly used terms */ - Node d_zero; - Node d_one; - Node d_neg_one; - Node d_true; - Node d_false; - /** - * 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 d_trMaster; - std::map> d_trSlaves; - /** The transcendental functions we have done initial refinements on */ - std::map d_tf_initial_refine; - - /** concavity region for transcendental functions - * - * This stores an integer that identifies an interval in - * which the current model value for an argument of an - * application of a transcendental function resides. - * - * For exp( x ): - * region #1 is -infty < x < infty - * For sin( x ): - * region #0 is pi < x < infty (this is an invalid region) - * region #1 is pi/2 < x <= pi - * region #2 is 0 < x <= pi/2 - * region #3 is -pi/2 < x <= 0 - * region #4 is -pi < x <= -pi/2 - * region #5 is -infty < x <= -pi (this is an invalid region) - * All regions not listed above, as well as regions 0 and 5 - * for SINE are "invalid". We only process applications - * of transcendental functions whose arguments have model - * values that reside in valid regions. - */ - std::unordered_map d_tf_region; - /** cache of the above function */ - std::map>> d_poly_bounds; - - /** - * 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> d_funcCongClass; - /** - * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } - * that are representives of their congruence class. - */ - std::map> d_funcMap; - - // tangent plane bounds - std::map> d_tangent_val_bound[4]; - - /** secant points (sorted list) for transcendental functions - * - * This is used for tangent plane refinements for - * transcendental functions. This is the set - * "get-previous-secant-points" in "Satisfiability - * Modulo Transcendental Functions via Incremental - * Linearization" by Cimatti et al., CADE 2017, for - * each transcendental function application. We store this set for each - * Taylor degree. - */ - std::unordered_map>, - NodeHashFunction> - d_secant_points; - - /** get Taylor series of degree n for function fa centered around point fa[0]. - * - * Return value is ( P_{n,f(a)}( x ), R_{n+1,f(a)}( x ) ) where - * the first part of the pair is the Taylor series expansion : - * P_{n,f(a)}( x ) = sum_{i=0}^n (f^i( a )/i!)*(x-a)^i - * and the second part of the pair is the Taylor series remainder : - * R_{n+1,f(a),b}( x ) = (f^{n+1}( b )/(n+1)!)*(x-a)^{n+1} - * - * The above values are cached for each (f,n) for a fixed variable "a". - * To compute the Taylor series for fa, we compute the Taylor series - * for ( fa.getKind(), n ) then substitute { a -> fa[0] } if fa[0]!=0. - * We compute P_{n,f(0)}( x )/R_{n+1,f(0),b}( x ) for ( fa.getKind(), n ) - * if fa[0]=0. - * In the latter case, note we compute the exponential x^{n+1} - * instead of (x-a)^{n+1}, which can be done faster. - */ - std::pair getTaylor(Node fa, unsigned n); - - /** internal variables used for constructing (cached) versions of the Taylor - * series above. - */ - Node d_taylor_real_fv; // x above - Node d_taylor_real_fv_base; // a above - Node d_taylor_real_fv_base_rem; // b above - - /** cache of sum and remainder terms for getTaylor */ - std::unordered_map, NodeHashFunction> - d_taylor_sum; - std::unordered_map, NodeHashFunction> - d_taylor_rem; - /** taylor degree - * - * Indicates that the degree of the polynomials in the Taylor approximation of - * all transcendental functions is 2*d_taylor_degree. This value is set - * initially to options::nlExtTfTaylorDegree() and may be incremented - * if the option options::nlExtTfIncPrecision() is enabled. - */ - unsigned d_taylor_degree; - /** PI - * - * Note that PI is a (symbolic, non-constant) nullary operator. This is - * because its value cannot be computed exactly. We constraint PI to concrete - * lower and upper bounds stored in d_pi_bound below. - */ - Node d_pi; - /** PI/2 */ - Node d_pi_2; - /** -PI/2 */ - Node d_pi_neg_2; - /** -PI */ - Node d_pi_neg; - /** the concrete lower and upper bounds for PI */ - Node d_pi_bound[2]; -}; /* class TranscendentalSolver */ - -} // namespace nl -} // namespace arith -} // namespace theory -} // namespace CVC4 - -#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ -- cgit v1.2.3 From 03979b02fb0296aefdfeb0c00e6eb4ea5ac01cc8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 00:30:56 -0600 Subject: Allow printing of null node in let binder (#5523) --- src/printer/let_binding.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp index 439037b64..2efc98318 100644 --- a/src/printer/let_binding.cpp +++ b/src/printer/let_binding.cpp @@ -30,8 +30,7 @@ uint32_t LetBinding::getThreshold() const { return d_thresh; } void LetBinding::process(Node n) { - Assert(!n.isNull()); - if (d_thresh == 0) + if (n.isNull() || d_thresh == 0) { // value of 0 means do not introduce let return; @@ -42,7 +41,6 @@ void LetBinding::process(Node n) void LetBinding::letify(Node n, std::vector& letList) { - Assert(!n.isNull()); // first, push the context pushScope(); // process the node -- cgit v1.2.3 From de14432ebd850dab001bb860db102e86ec734f97 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 10:46:41 -0600 Subject: Use symbol manager for printing responses get-model (#5516) This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags. This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model. This is one of the last remaining steps for migrating the parser to the new API. The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc. --- src/parser/parser.cpp | 15 +- src/printer/ast/ast_printer.cpp | 19 ++- src/printer/ast/ast_printer.h | 20 ++- src/printer/cvc/cvc_printer.cpp | 85 ++++------ src/printer/cvc/cvc_printer.h | 20 ++- src/printer/printer.cpp | 30 +++- src/printer/printer.h | 27 ++-- src/printer/smt2/smt2_printer.cpp | 173 +++++++++------------ src/printer/smt2/smt2_printer.h | 21 ++- src/printer/tptp/tptp_printer.cpp | 19 ++- src/printer/tptp/tptp_printer.h | 18 ++- src/smt/command.cpp | 20 ++- src/smt/node_command.cpp | 3 +- .../regress0/datatypes/dt-param-2.6-print.smt2 | 1 - test/unit/parser/parser_black.h | 2 - 15 files changed, 247 insertions(+), 226 deletions(-) diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1fc995fd6..1ca2e1c01 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -333,8 +333,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 = - api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags)); + api::Sort type = d_solver->mkUninterpretedSort(name); bool globalDecls = d_symman->getGlobalDeclarations(); defineType( name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); @@ -347,9 +346,7 @@ api::Sort Parser::mkSortConstructor(const std::string& name, { Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = api::Sort( - d_solver, - d_solver->getExprManager()->mkSortConstructor(name, arity, flags)); + api::Sort type = d_solver->mkSortConstructorSort(name, arity); bool globalDecls = d_symman->getGlobalDeclarations(); defineType(name, vector(arity), @@ -379,10 +376,7 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = - api::Sort(d_solver, - d_solver->getExprManager()->mkSortConstructor( - name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER)); + api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size()); defineType(name, params, unresolved); api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); @@ -644,8 +638,7 @@ api::Term Parser::mkVar(const std::string& name, const api::Sort& type, uint32_t flags) { - return api::Term( - d_solver, d_solver->getExprManager()->mkVar(name, type.getType(), flags)); + return d_solver->mkConst(type, name); } //!!!!!!!!!!! temporary diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 8bf3bd24e..4b9371181 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -148,9 +148,17 @@ void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const out << "Model()"; } -void AstPrinter::toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const +void AstPrinter::toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const +{ + // shouldn't be called; only the non-Command* version above should be + Unreachable(); +} + +void AstPrinter::toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const { // shouldn't be called; only the non-Command* version above should be Unreachable(); @@ -272,12 +280,9 @@ void AstPrinter::toStreamCmdDefineFunction(std::ostream& out, } void AstPrinter::toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const { - out << "DeclareType(" << id << "," << arity << "," << type << ')' - << std::endl; + out << "DeclareType(" << type << ')' << std::endl; } void AstPrinter::toStreamCmdDefineType(std::ostream& out, diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index ad20ffb79..e4251eba0 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -62,8 +62,6 @@ class AstPrinter : public CVC4::Printer /** Print declare-sort command */ void toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const override; /** Print define-sort command */ @@ -165,9 +163,21 @@ class AstPrinter : public CVC4::Printer private: void toStream(std::ostream& out, TNode n, int toDepth) const; - void toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const override; + /** + * To stream model sort. This prints the appropriate output for type + * tn declared via declare-sort or declare-datatype. + */ + void toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const override; + + /** + * To stream model term. This prints the appropriate output for term + * n declared via declare-fun. + */ + void toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const override; }; /* class AstPrinter */ } // namespace ast diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 44ff7be10..be530099b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1067,20 +1067,23 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const }/* CvcPrinter::toStream(CommandStatus*) */ -namespace { - -void DeclareTypeNodeCommandToStream(std::ostream& out, - const theory::TheoryModel& model, - const DeclareTypeNodeCommand& command) +void CvcPrinter::toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const { - TypeNode type_node = command.getType(); - const std::vector* type_reps = - model.getRepSet()->getTypeRepsOrNull(type_node); + if (!tn.isSort()) + { + out << "ERROR: don't know how to print a non uninterpreted sort in model: " + << tn << std::endl; + return; + } + const theory::TheoryModel* tm = m.getTheoryModel(); + const std::vector* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn); if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum - && type_node.isSort() && type_reps != nullptr) + && type_reps != nullptr) { out << "DATATYPE" << std::endl; - out << " " << command.getSymbol() << " = "; + out << " " << tn << " = "; for (size_t i = 0; i < type_reps->size(); i++) { if (i > 0) @@ -1091,16 +1094,16 @@ void DeclareTypeNodeCommandToStream(std::ostream& out, } out << std::endl << "END;" << std::endl; } - else if (type_node.isSort() && type_reps != nullptr) + else if (type_reps != nullptr) { - out << "% cardinality of " << type_node << " is " << type_reps->size() + out << "% cardinality of " << tn << " is " << type_reps->size() << std::endl; - out << command << std::endl; + toStreamCmdDeclareType(out, tn); for (Node type_rep : *type_reps) { if (type_rep.isVar()) { - out << type_rep << " : " << type_node << ";" << std::endl; + out << type_rep << " : " << tn << ";" << std::endl; } else { @@ -1110,21 +1113,15 @@ void DeclareTypeNodeCommandToStream(std::ostream& out, } else { - out << command << std::endl; + toStreamCmdDeclareType(out, tn); } } -void DeclareFunctionNodeCommandToStream( - std::ostream& out, - const theory::TheoryModel& model, - const DeclareFunctionNodeCommand& command) +void CvcPrinter::toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const { - Node n = command.getFunction(); - if (n.getKind() == kind::SKOLEM) - { - // don't print out internal stuff - return; - } + const theory::TheoryModel* tm = m.getTheoryModel(); TypeNode tn = n.getType(); out << n << " : "; if (tn.isFunction() || tn.isPredicate()) @@ -1146,15 +1143,16 @@ void DeclareFunctionNodeCommandToStream( } // We get the value from the theory model directly, which notice // does not have to go through the standard SmtEngine::getValue interface. - Node val = model.getValue(n); + Node val = tm->getValue(n); if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum && val.getKind() == kind::STORE) { TypeNode type_node = val[1].getType(); if (tn.isSort()) { - if (const std::vector* type_reps = - model.getRepSet()->getTypeRepsOrNull(type_node)) + const std::vector* type_reps = + tm->getRepSet()->getTypeRepsOrNull(type_node); + if (type_reps != nullptr) { Cardinality indexCard(type_reps->size()); val = theory::arrays::TheoryArraysRewriter::normalizeConstant( @@ -1165,8 +1163,6 @@ void DeclareFunctionNodeCommandToStream( out << " = " << val << ";" << std::endl; } -} // namespace - void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const { const theory::TheoryModel* tm = m.getTheoryModel(); @@ -1185,28 +1181,6 @@ void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const out << "MODEL END;" << std::endl; } -void CvcPrinter::toStream(std::ostream& out, - const smt::Model& model, - const NodeCommand* command) const -{ - const auto* theory_model = model.getTheoryModel(); - AlwaysAssert(theory_model != nullptr); - if (const auto* declare_type_command = - dynamic_cast(command)) - { - DeclareTypeNodeCommandToStream(out, *theory_model, *declare_type_command); - } - else if (const auto* dfc = - dynamic_cast(command)) - { - DeclareFunctionNodeCommandToStream(out, *theory_model, *dfc); - } - else - { - out << *command << std::endl; - } -} - void CvcPrinter::toStreamCmdAssert(std::ostream& out, Node n) const { out << "ASSERT " << n << ';' << std::endl; @@ -1322,6 +1296,7 @@ void CvcPrinter::toStreamCmdDeclarationSequence( { DeclarationDefinitionCommand* dd = static_cast(*i++); + Assert(dd != nullptr); if (i != sequence.cend()) { out << dd->getSymbol() << ", "; @@ -1376,20 +1351,18 @@ void CvcPrinter::toStreamCmdDefineFunction(std::ostream& out, } void CvcPrinter::toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const { + size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0; if (arity > 0) { - // TODO? out << "ERROR: Don't know how to print parameterized type declaration " "in CVC language." << std::endl; } else { - out << id << " : TYPE;" << std::endl; + out << type << " : TYPE;" << std::endl; } } diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index ee4750a61..b0328bc3c 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -63,8 +63,6 @@ class CvcPrinter : public CVC4::Printer /** Print declare-sort command */ void toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const override; /** Print define-sort command */ @@ -166,9 +164,21 @@ class CvcPrinter : public CVC4::Printer private: void toStream(std::ostream& out, TNode n, int toDepth, bool bracket) const; - void toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const override; + /** + * To stream model sort. This prints the appropriate output for type + * tn declared via declare-sort or declare-datatype. + */ + void toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const override; + + /** + * To stream model term. This prints the appropriate output for term + * n declared via declare-fun. + */ + void toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const override; bool d_cvc3Mode; }; /* class CvcPrinter */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index b24025124..7225721c0 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -74,18 +74,34 @@ unique_ptr Printer::makePrinter(OutputLanguage lang) void Printer::toStream(std::ostream& out, const smt::Model& m) const { - for(size_t i = 0; i < m.getNumCommands(); ++i) { - const NodeCommand* cmd = m.getCommand(i); - const DeclareFunctionNodeCommand* dfc = - dynamic_cast(cmd); - if (dfc != NULL && !m.isModelCoreSymbol(dfc->getFunction())) + // print the declared sorts + const std::vector& dsorts = m.getDeclaredSorts(); + for (const TypeNode& tn : dsorts) + { + toStreamModelSort(out, m, tn); + } + + // print the declared terms + const std::vector& dterms = m.getDeclaredTerms(); + for (const Node& n : dterms) + { + // take into account model core, independently of the format + if (!m.isModelCoreSymbol(n)) { continue; } - toStream(out, m, cmd); + toStreamModelTerm(out, m, n); } + }/* Printer::toStream(Model) */ +void Printer::toStreamUsing(OutputLanguage lang, + std::ostream& out, + const smt::Model& m) const +{ + getPrinter(lang)->toStream(out, m); +} + void Printer::toStream(std::ostream& out, const UnsatCore& core) const { for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) { @@ -160,8 +176,6 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, } void Printer::toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const { printUnknownCommand(out, "declare-sort"); diff --git a/src/printer/printer.h b/src/printer/printer.h index d32418deb..5bcccedb8 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -86,8 +86,6 @@ class Printer /** Print declare-sort command */ virtual void toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const; /** Print define-sort command */ @@ -266,19 +264,26 @@ class Printer /** Derived classes can construct, but no one else. */ Printer() {} - /** write model response to command */ - virtual void toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const = 0; + /** + * To stream model sort. This prints the appropriate output for type + * tn declared via declare-sort or declare-datatype. + */ + virtual void toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const = 0; + + /** + * To stream model term. This prints the appropriate output for term + * n declared via declare-fun. + */ + virtual void toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const = 0; /** write model response to command using another language printer */ void toStreamUsing(OutputLanguage lang, std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const - { - getPrinter(lang)->toStream(out, m, c); - } + const smt::Model& m) const; /** * Write an error to `out` stating that command `name` is not supported by diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 747873bee..9e9500bdb 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1364,124 +1364,91 @@ void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const } } -void Smt2Printer::toStream(std::ostream& out, - const smt::Model& model, - const NodeCommand* command) const +void Smt2Printer::toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const { - const theory::TheoryModel* theory_model = model.getTheoryModel(); - AlwaysAssert(theory_model != nullptr); - if (const DeclareTypeNodeCommand* dtc = - dynamic_cast(command)) + if (!tn.isSort()) { - // print out the DeclareTypeCommand - TypeNode tn = dtc->getType(); - if (!tn.isSort()) + out << "ERROR: don't know how to print non uninterpreted sort in model: " + << tn << std::endl; + return; + } + const theory::TheoryModel* tm = m.getTheoryModel(); + std::vector elements = tm->getDomainElements(tn); + if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum) + { + if (isVariant_2_6(d_variant)) { - out << (*dtc) << endl; + out << "(declare-datatypes ((" << tn << " 0)) ("; } else { - std::vector elements = theory_model->getDomainElements(tn); - if (options::modelUninterpPrint() - == options::ModelUninterpPrintMode::DtEnum) - { - if (isVariant_2_6(d_variant)) - { - out << "(declare-datatypes ((" << (*dtc).getSymbol() << " 0)) ("; - } - else - { - out << "(declare-datatypes () ((" << (*dtc).getSymbol() << " "; - } - for (const Node& type_ref : elements) - { - out << "(" << type_ref << ")"; - } - out << ")))" << endl; - } - else - { - // print the cardinality - out << "; cardinality of " << tn << " is " << elements.size() << endl; - if (options::modelUninterpPrint() - == options::ModelUninterpPrintMode::DeclSortAndFun) - { - out << (*dtc) << endl; - } - // print the representatives - for (const Node& trn : elements) - { - if (trn.isVar()) - { - out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")" - << endl; - } - else - { - out << "; rep: " << trn << endl; - } - } - } - } - } - else if (const DeclareFunctionNodeCommand* dfc = - dynamic_cast(command)) - { - // print out the DeclareFunctionCommand - Node n = dfc->getFunction(); - if ((*dfc).getPrintInModelSetByUser()) - { - if (!(*dfc).getPrintInModel()) - { - return; - } + out << "(declare-datatypes () ((" << tn << " "; } - else if (n.getKind() == kind::SKOLEM) + for (const Node& type_ref : elements) { - // don't print out internal stuff - return; + out << "(" << type_ref << ")"; } - // We get the value from the theory model directly, which notice - // does not have to go through the standard SmtEngine::getValue interface. - Node val = theory_model->getValue(n); - if (val.getKind() == kind::LAMBDA) + out << ")))" << endl; + return; + } + // print the cardinality + out << "; cardinality of " << tn << " is " << elements.size() << endl; + if (options::modelUninterpPrint() + == options::ModelUninterpPrintMode::DeclSortAndFun) + { + toStreamCmdDeclareType(out, tn); + } + // print the representatives + for (const Node& trn : elements) + { + if (trn.isVar()) { - TypeNode rangeType = n.getType().getRangeType(); - out << "(define-fun " << n << " " << val[0] << " " << rangeType << " "; - // call toStream and force its type to be proper - toStreamCastToType(out, val[1], -1, rangeType); - out << ")" << endl; + out << "(declare-fun " << quoteSymbol(trn) << " () " << tn << ")" << endl; } else { - if (options::modelUninterpPrint() - == options::ModelUninterpPrintMode::DtEnum - && val.getKind() == kind::STORE) - { - TypeNode tn = val[1].getType(); - const std::vector* type_refs = - theory_model->getRepSet()->getTypeRepsOrNull(tn); - if (tn.isSort() && type_refs != nullptr) - { - Cardinality indexCard(type_refs->size()); - val = theory::arrays::TheoryArraysRewriter::normalizeConstant( - val, indexCard); - } - } - out << "(define-fun " << n << " () " << n.getType() << " "; - // call toStream and force its type to be proper - toStreamCastToType(out, val, -1, n.getType()); - out << ")" << endl; + out << "; rep: " << trn << endl; } } - else if (const DeclareDatatypeNodeCommand* declare_datatype_command = - dynamic_cast(command)) +} + +void Smt2Printer::toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const +{ + const theory::TheoryModel* tm = m.getTheoryModel(); + // We get the value from the theory model directly, which notice + // does not have to go through the standard SmtEngine::getValue interface. + Node val = tm->getValue(n); + if (val.getKind() == kind::LAMBDA) { - out << *declare_datatype_command; + TypeNode rangeType = n.getType().getRangeType(); + out << "(define-fun " << n << " " << val[0] << " " << rangeType << " "; + // call toStream and force its type to be proper + toStreamCastToType(out, val[1], -1, rangeType); + out << ")" << endl; } else { - Unreachable(); + if (options::modelUninterpPrint() == options::ModelUninterpPrintMode::DtEnum + && val.getKind() == kind::STORE) + { + TypeNode tn = val[1].getType(); + const std::vector* type_refs = + tm->getRepSet()->getTypeRepsOrNull(tn); + if (tn.isSort() && type_refs != nullptr) + { + Cardinality indexCard(type_refs->size()); + val = theory::arrays::TheoryArraysRewriter::normalizeConstant( + val, indexCard); + } + } + out << "(define-fun " << n << " () " << n.getType() << " "; + // call toStream and force its type to be proper + toStreamCastToType(out, val, -1, n.getType()); + out << ")" << endl; } } @@ -1694,11 +1661,13 @@ void Smt2Printer::toStreamCmdDefineFunctionRec( } void Smt2Printer::toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const { - out << "(declare-sort " << CVC4::quoteSymbol(id) << " " << arity << ")" + Assert(type.isSort() || type.isSortConstructor()); + std::stringstream id; + id << type; + size_t arity = type.isSortConstructor() ? type.getSortConstructorArity() : 0; + out << "(declare-sort " << CVC4::quoteSymbol(id.str()) << " " << arity << ")" << std::endl; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index c83a74d97..3d90cee06 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -78,8 +78,6 @@ class Smt2Printer : public CVC4::Printer /** Print declare-sort command */ void toStreamCmdDeclareType(std::ostream& out, - const std::string& id, - size_t arity, TypeNode type) const override; /** Print define-sort command */ @@ -243,11 +241,24 @@ class Smt2Printer : public CVC4::Printer TNode n, int toDepth, TypeNode tn) const; - void toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const override; void toStream(std::ostream& out, const SExpr& sexpr) const; void toStream(std::ostream& out, const DType& dt) const; + /** + * To stream model sort. This prints the appropriate output for type + * tn declared via declare-sort or declare-datatype. + */ + void toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const override; + + /** + * To stream model term. This prints the appropriate output for term + * n declared via declare-fun. + */ + void toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const override; + /** * To stream with let binding. This prints n, possibly in the scope * of letification generated by this method based on lbind. diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index c93f3593a..f9384b0cb 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -54,20 +54,27 @@ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const : "CandidateFiniteModel"); out << "% SZS output start " << statusName << " for " << m.getInputName() << endl; - for(size_t i = 0; i < m.getNumCommands(); ++i) { - this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m, m.getCommand(i)); - } + this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_5, out, m); out << "% SZS output end " << statusName << " for " << m.getInputName() << endl; } -void TptpPrinter::toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const +void TptpPrinter::toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const +{ + // shouldn't be called; only the non-Command* version above should be + Unreachable(); +} + +void TptpPrinter::toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const { // shouldn't be called; only the non-Command* version above should be Unreachable(); } + void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const { out << "% SZS output start UnsatCore " << std::endl; diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 449fe409c..38a56bcb5 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -44,9 +44,21 @@ class TptpPrinter : public CVC4::Printer void toStream(std::ostream& out, const UnsatCore& core) const override; private: - void toStream(std::ostream& out, - const smt::Model& m, - const NodeCommand* c) const override; + /** + * To stream model sort. This prints the appropriate output for type + * tn declared via declare-sort or declare-datatype. + */ + void toStreamModelSort(std::ostream& out, + const smt::Model& m, + TypeNode tn) const override; + + /** + * To stream model term. This prints the appropriate output for term + * n declared via declare-fun. + */ + void toStreamModelTerm(std::ostream& out, + const smt::Model& m, + Node n) const override; }; /* class TptpPrinter */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 717d423fe..154166eb7 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1091,6 +1091,8 @@ void DeclareFunctionCommand::setPrintInModel(bool p) void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { + // mark that it will be printed in the model + sm->addModelDeclarationTerm(d_func); d_commandStatus = CommandSuccess::instance(); } @@ -1132,6 +1134,8 @@ size_t DeclareSortCommand::getArity() const { return d_arity; } api::Sort DeclareSortCommand::getSort() const { return d_sort; } void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm) { + // mark that it will be printed in the model + sm->addModelDeclarationSort(d_sort); d_commandStatus = CommandSuccess::instance(); } @@ -1150,8 +1154,8 @@ void DeclareSortCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdDeclareType( - out, d_sort.toString(), d_arity, d_sort.getTypeNode()); + Printer::getPrinter(language)->toStreamCmdDeclareType(out, + d_sort.getTypeNode()); } /* -------------------------------------------------------------------------- */ @@ -1693,6 +1697,18 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) try { d_result = solver->getSmtEngine()->getModel(); + // set the model declarations, which determines what is printed in the model + d_result->clearModelDeclarations(); + std::vector declareSorts = sm->getModelDeclareSorts(); + for (const api::Sort& s : declareSorts) + { + d_result->addDeclarationSort(s.getTypeNode()); + } + std::vector declareTerms = sm->getModelDeclareTerms(); + for (const api::Term& t : declareTerms) + { + d_result->addDeclarationTerm(t.getNode()); + } d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index eb2493c87..91184d27d 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -104,8 +104,7 @@ void DeclareTypeNodeCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdDeclareType( - out, d_id, d_arity, d_type); + Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type); } NodeCommand* DeclareTypeNodeCommand::clone() const diff --git a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 index 2b706478f..ce92821c1 100644 --- a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 +++ b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 @@ -1,6 +1,5 @@ ; EXPECT: sat ; EXPECT: ( -; EXPECT: (declare-datatypes ((Pair 2)) ((par (X Y)((mkPair (first X) (second Y)))))) ; EXPECT: (define-fun x () (Pair Int Real) ((as mkPair (Pair Int Real)) 2 (/ 3 2))) ; EXPECT: ) diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 3b0bbb139..ef8f2e3cf 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -259,8 +259,6 @@ public: tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a' - //tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges - tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];"); tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;"); tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;"); //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); -- cgit v1.2.3 From 192c6c7667f74c91f4769b009cf8acc131292098 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 25 Nov 2020 19:07:54 +0100 Subject: Fix transcendental secant plane lemmas (#5525) The refactoring of the transcendental solver introduced a subtle issue that lead to incorrect secant plane lemmas. This PR fixes this issue, so that we now produce the correct lemmas again. --- .../arith/nl/transcendental/exponential_solver.cpp | 9 +- .../arith/nl/transcendental/exponential_solver.h | 3 +- src/theory/arith/nl/transcendental/sine_solver.cpp | 11 +- src/theory/arith/nl/transcendental/sine_solver.h | 8 +- .../nl/transcendental/transcendental_solver.cpp | 4 +- .../nl/transcendental/transcendental_state.cpp | 22 ++- .../arith/nl/transcendental/transcendental_state.h | 209 +++++++++++---------- 7 files changed, 143 insertions(+), 123 deletions(-) diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 4275b2487..7d7d0c23c 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -170,12 +170,11 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); } -void ExponentialSolver::doSecantLemmas(TNode e, - TNode c, - TNode poly_approx, - unsigned d) +void ExponentialSolver::doSecantLemmas( + TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d) { - d_data->doSecantLemmas(getSecantBounds(e, c, d), c, poly_approx, e, d, 1); + d_data->doSecantLemmas( + getSecantBounds(e, c, d), poly_approx, c, poly_approx_c, e, d, 1); } std::pair ExponentialSolver::getSecantBounds(TNode e, diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index f757e5892..b20c23e56 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -87,7 +87,8 @@ class ExponentialSolver void doTangentLemma(TNode e, TNode c, TNode poly_approx); /** Sent secant lemmas around c for e */ - void doSecantLemmas(TNode e, TNode c, TNode poly_approx, unsigned d); + void doSecantLemmas( + TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d); private: /** Generate bounds for secant lemmas */ diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 012b8e7ec..31fd47503 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -289,12 +289,17 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region) d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); } -void SineSolver::doSecantLemmas( - TNode e, TNode c, TNode poly_approx, unsigned d, int region) +void SineSolver::doSecantLemmas(TNode e, + TNode poly_approx, + TNode c, + TNode poly_approx_c, + unsigned d, + int region) { d_data->doSecantLemmas(getSecantBounds(e, c, d, region), - c, poly_approx, + c, + poly_approx_c, e, d, regionToConcavity(region)); diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index 394c2d927..9f9102a53 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -88,8 +88,12 @@ class SineSolver void doTangentLemma(TNode e, TNode c, TNode poly_approx, int region); /** Sent secant lemmas around c for e */ - void doSecantLemmas( - TNode e, TNode c, TNode poly_approx, unsigned d, int region); + void doSecantLemmas(TNode e, + TNode poly_approx, + TNode c, + TNode poly_approx_c, + unsigned d, + int region); private: std::pair getSecantBounds(TNode e, diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 1f76cd833..8eb69e50b 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -362,11 +362,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) { if (k == EXPONENTIAL) { - d_expSlv.doSecantLemmas(tf, c, poly_approx_c, d); + d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d); } else if (k == Kind::SINE) { - d_sineSlv.doSecantLemmas(tf, c, poly_approx_c, d, region); + d_sineSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, region); } } return true; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index b6882d606..41ed2c53d 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -294,12 +294,9 @@ std::pair TranscendentalState::getClosestSecantPoints(TNode e, } Node TranscendentalState::mkSecantPlane( - TNode arg, TNode b, TNode c, TNode approx, TNode approx_c) + TNode arg, TNode b, TNode c, TNode approx_b, TNode approx_c) { NodeManager* nm = NodeManager::currentNM(); - // Figure 3 : P(l), P(u), for s = 0,1 - Node approx_b = - Rewriter::rewrite(approx.substitute(d_taylor.getTaylorVariable(), b)); // Figure 3: S_l( x ), S_u( x ) for s = 0,1 Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, b, c)); Assert(rcoeff_n.isConst()); @@ -345,18 +342,26 @@ NlLemma TranscendentalState::mkSecantLemma( } void TranscendentalState::doSecantLemmas(const std::pair& bounds, + TNode poly_approx, TNode c, TNode approx_c, TNode tf, unsigned d, int concavity) { + Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds.first + << " ... " << bounds.second << std::endl; // take the model value of l or u (since may contain PI) // Make secant from bounds.first to c Node lval = d_model.computeAbstractModelValue(bounds.first); + Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.first + << " is " << lval << std::endl; if (lval != c) { - Node splane = mkSecantPlane(tf[0], lval, c, bounds.first, approx_c); + // Figure 3 : P(l), P(u), for s = 0 + Node approx_l = Rewriter::rewrite( + poly_approx.substitute(d_taylor.getTaylorVariable(), lval)); + Node splane = mkSecantPlane(tf[0], lval, c, approx_l, approx_c); NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). @@ -366,9 +371,14 @@ void TranscendentalState::doSecantLemmas(const std::pair& bounds, // Make secant from c to bounds.second Node uval = d_model.computeAbstractModelValue(bounds.second); + Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.second + << " is " << uval << std::endl; if (c != uval) { - Node splane = mkSecantPlane(tf[0], c, uval, approx_c, bounds.second); + // Figure 3 : P(l), P(u), for s = 1 + Node approx_u = Rewriter::rewrite( + poly_approx.substitute(d_taylor.getTaylorVariable(), uval)); + Node splane = mkSecantPlane(tf[0], c, uval, approx_c, approx_u); NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 2cf6400a3..0a4e46eca 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -89,6 +89,7 @@ struct TranscendentalState /** * Construct and send secant lemmas (if appropriate) * @param bounds Secant bounds + * @param poly_approx Polynomial approximation * @param c Current point * @param approx_c Approximation for c * @param tf Current transcendental term @@ -96,118 +97,118 @@ struct TranscendentalState * @param concavity Concavity in region of c */ void doSecantLemmas(const std::pair& bounds, + TNode poly_approx, TNode c, TNode approx_c, TNode tf, unsigned d, - int concavity) - ; - - Node d_true; - Node d_false; - Node d_zero; - Node d_one; - Node d_neg_one; - - /** The inference manager that we push conflicts and lemmas to. */ - InferenceManager& d_im; - /** Reference to the non-linear model object */ - NlModel& d_model; - /** Utility to compute taylor approximations */ - TaylorGenerator d_taylor; - - /** - * 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 d_trMaster; - std::map> d_trSlaves; - - /** concavity region for transcendental functions - * - * This stores an integer that identifies an interval in - * which the current model value for an argument of an - * application of a transcendental function resides. - * - * For exp( x ): - * region #1 is -infty < x < infty - * For sin( x ): - * region #0 is pi < x < infty (this is an invalid region) - * region #1 is pi/2 < x <= pi - * region #2 is 0 < x <= pi/2 - * region #3 is -pi/2 < x <= 0 - * region #4 is -pi < x <= -pi/2 - * region #5 is -infty < x <= -pi (this is an invalid region) - * All regions not listed above, as well as regions 0 and 5 - * for SINE are "invalid". We only process applications - * of transcendental functions whose arguments have model - * values that reside in valid regions. - */ - std::unordered_map d_tf_region; - /** - * 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> d_funcCongClass; - /** - * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } - * that are representives of their congruence class. - */ - std::map> d_funcMap; - - /** secant points (sorted list) for transcendental functions - * - * This is used for tangent plane refinements for - * transcendental functions. This is the set - * "get-previous-secant-points" in "Satisfiability - * Modulo Transcendental Functions via Incremental - * Linearization" by Cimatti et al., CADE 2017, for - * each transcendental function application. We store this set for each - * Taylor degree. - */ - std::unordered_map>, - NodeHashFunction> - d_secant_points; - - /** PI - * - * Note that PI is a (symbolic, non-constant) nullary operator. This is - * because its value cannot be computed exactly. We constraint PI to - * concrete lower and upper bounds stored in d_pi_bound below. - */ - Node d_pi; - /** PI/2 */ - Node d_pi_2; - /** -PI/2 */ - Node d_pi_neg_2; - /** -PI */ - Node d_pi_neg; - /** the concrete lower and upper bounds for PI */ - Node d_pi_bound[2]; - }; + int concavity); + + Node d_true; + Node d_false; + Node d_zero; + Node d_one; + Node d_neg_one; + + /** The inference manager that we push conflicts and lemmas to. */ + InferenceManager& d_im; + /** Reference to the non-linear model object */ + NlModel& d_model; + /** Utility to compute taylor approximations */ + TaylorGenerator d_taylor; + + /** + * 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 d_trMaster; + std::map> d_trSlaves; + + /** concavity region for transcendental functions + * + * This stores an integer that identifies an interval in + * which the current model value for an argument of an + * application of a transcendental function resides. + * + * For exp( x ): + * region #1 is -infty < x < infty + * For sin( x ): + * region #0 is pi < x < infty (this is an invalid region) + * region #1 is pi/2 < x <= pi + * region #2 is 0 < x <= pi/2 + * region #3 is -pi/2 < x <= 0 + * region #4 is -pi < x <= -pi/2 + * region #5 is -infty < x <= -pi (this is an invalid region) + * All regions not listed above, as well as regions 0 and 5 + * for SINE are "invalid". We only process applications + * of transcendental functions whose arguments have model + * values that reside in valid regions. + */ + std::unordered_map d_tf_region; + /** + * 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> d_funcCongClass; + /** + * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } + * that are representives of their congruence class. + */ + std::map> d_funcMap; + + /** secant points (sorted list) for transcendental functions + * + * This is used for tangent plane refinements for + * transcendental functions. This is the set + * "get-previous-secant-points" in "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017, for + * each transcendental function application. We store this set for each + * Taylor degree. + */ + std::unordered_map>, + NodeHashFunction> + d_secant_points; + + /** PI + * + * Note that PI is a (symbolic, non-constant) nullary operator. This is + * because its value cannot be computed exactly. We constraint PI to + * concrete lower and upper bounds stored in d_pi_bound below. + */ + Node d_pi; + /** PI/2 */ + Node d_pi_2; + /** -PI/2 */ + Node d_pi_neg_2; + /** -PI */ + Node d_pi_neg; + /** the concrete lower and upper bounds for PI */ + Node d_pi_bound[2]; +}; -} // namespace transcendental } // namespace transcendental } // namespace nl } // namespace arith } // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */ -- cgit v1.2.3 From 8e21ca2de274f82ded4429d21a34741fc1501b1b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 13:35:58 -0600 Subject: Add regressions for closed issues (#5526) We can close #5520, we can close #5378. --- test/regress/CMakeLists.txt | 4 ++++ test/regress/regress1/arith/issue4985-model-success.smt2 | 7 +++++++ test/regress/regress1/arith/issue4985b-model-success.smt2 | 6 ++++++ test/regress/regress1/quantifiers/issue5378-witness.smt2 | 5 +++++ test/regress/regress1/strings/issue5520-re-consume.smt2 | 12 ++++++++++++ 5 files changed, 34 insertions(+) create mode 100644 test/regress/regress1/arith/issue4985-model-success.smt2 create mode 100644 test/regress/regress1/arith/issue4985b-model-success.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5378-witness.smt2 create mode 100644 test/regress/regress1/strings/issue5520-re-consume.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f66dc2d10..effe70c1c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1283,6 +1283,8 @@ set(regress_1_tests regress1/arith/div.08.smt2 regress1/arith/div.09.smt2 regress1/arith/issue3952-rew-eq.smt2 + regress1/arith/issue4985-model-success.smt2 + regress1/arith/issue4985b-model-success.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc regress1/arith/mod.02.smt2 @@ -1613,6 +1615,7 @@ set(regress_1_tests regress1/quantifiers/issue5019-cegqi-i.smt2 regress1/quantifiers/issue5279-nqe.smt2 regress1/quantifiers/issue5365-nqe.smt2 + regress1/quantifiers/issue5378-witness.smt2 regress1/quantifiers/issue5469-aext.smt2 regress1/quantifiers/issue5470-aext.smt2 regress1/quantifiers/issue5471-aext.smt2 @@ -1864,6 +1867,7 @@ set(regress_1_tests regress1/strings/issue5374-proxy-i.smt2 regress1/strings/issue5483-pp-leq.smt2 regress1/strings/issue5510-re-consume.smt2 + regress1/strings/issue5520-re-consume.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/arith/issue4985-model-success.smt2 b/test/regress/regress1/arith/issue4985-model-success.smt2 new file mode 100644 index 000000000..794eefb37 --- /dev/null +++ b/test/regress/regress1/arith/issue4985-model-success.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_AUFNRA) +(set-info :status sat) +(declare-const arr0 (Array Real Real)) +(declare-const r5 Real) +(declare-const r19 Real) +(assert (! (<= 0.0 0.0 48107.0 (- 6.7954749 0.0 6.7954749 0.0 (select arr0 (/ 40.87941 r5))) r19) :named IP_174)) +(check-sat) diff --git a/test/regress/regress1/arith/issue4985b-model-success.smt2 b/test/regress/regress1/arith/issue4985b-model-success.smt2 new file mode 100644 index 000000000..eae8d369d --- /dev/null +++ b/test/regress/regress1/arith/issue4985b-model-success.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_AUFNRA) +(set-info :status sat) +(declare-const a (Array Real Real)) +(declare-const r Real) +(assert (= 1.0 (select a (/ 2 r)))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue5378-witness.smt2 b/test/regress/regress1/quantifiers/issue5378-witness.smt2 new file mode 100644 index 000000000..b8628a432 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5378-witness.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --sygus-inst --strings-exp +; EXPECT: unsat +(set-logic ALL) +(assert (forall ((a Int) (b Int)) (or (> a (/ 0 b)) (exists ((c Int)) (< a c b))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue5520-re-consume.smt2 b/test/regress/regress1/strings/issue5520-re-consume.smt2 new file mode 100644 index 000000000..3fc4fe8e5 --- /dev/null +++ b/test/regress/regress1/strings/issue5520-re-consume.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_S) +(set-info :status sat) +(declare-fun x () String) +(assert + (not + (str.in_re (str.++ "a" x "ca") + (re.* + (re.++ (re.union (str.to_re "a") (str.to_re "b")) + (re.union (re.* (str.to_re "a")) (str.to_re "b") (str.to_re "c"))))))) +(check-sat) -- cgit v1.2.3 From 084518db641e0648164bbe4461cd98b10e937dc0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 20:37:23 -0600 Subject: Disable fact vs lemma optimization in datatypes for now (#5521) This optimization needs more work to determine its correctness. It is currently leading to incorrect candidate models on Facebook benchmarks. --- src/theory/datatypes/theory_datatypes.cpp | 17 +++++++++++------ test/regress/CMakeLists.txt | 3 ++- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6bfe136ce..74c822215 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1551,13 +1551,18 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ } eq = tt.eqNode(tt_cons); // Determine if the equality must be sent out as a lemma. Notice that - // we can keep new equalities from the instantiate rule internal as long as - // they are for datatype constructors that have no arguments that have - // finite external type. Such equalities must be sent because they introduce - // selector terms that may contribute to conflicts due to cardinality (good - // examples of this are regress0/datatypes/dt-param-card4-bool-sat.smt2 and + // we could potentially keep new equalities from the instantiate rule internal + // as long as they are for datatype constructors that have no arguments that + // have finite external type, which would correspond to: + // forceLemma = dt[index].hasFiniteExternalArgType(ttn); + // Such equalities must be sent because they introduce selector terms that + // may contribute to conflicts due to cardinality (good examples of this are + // regress0/datatypes/dt-param-card4-bool-sat.smt2 and // regress0/datatypes/list-bool.smt2). - bool forceLemma = dt[index].hasFiniteExternalArgType(ttn); + // For now, to be conservative, we always send lemmas out, since otherwise + // we may encounter conflicts during model building when datatypes adds its + // equality engine to the theory model. + bool forceLemma = true; Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq << " forceLemma = " << forceLemma << std::endl; d_im.addPendingInference(eq, exp, forceLemma, InferId::INST); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index effe70c1c..8969b6c01 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -769,7 +769,6 @@ set(regress_0_tests regress0/quantifiers/issue4086-infs.smt2 regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 regress0/quantifiers/issue4437-unc-quant.smt2 - regress0/quantifiers/issue4476-ext-rew.smt2 regress0/quantifiers/issue4576.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 @@ -2418,6 +2417,8 @@ set(regression_disabled_tests regress0/ite_arith.smt2 regress0/lemmas/fischer3-mutex-16.smtv1.smt2 regress0/nl/all-logic.smt2 + # timeout after change to datatypes, impacting sygus-inst + regress0/quantifiers/issue4476-ext-rew.smt2 regress0/quantifiers/qbv-multi-lit-uge.smt2 regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 -- cgit v1.2.3 From d0c352ec04846353d630073e78e5b2fea92133c2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 21:00:13 -0600 Subject: Fix missed case of theory preprocessing (#5531) This fixes a rare case of theory preprocessing where rewriting a quantified formula would introduce a term that would not be preprocessed. This led to solution unsoundness on a branch where the relationship between expand definitions and preprocessing is modified. This is required for updating to the new policy for expand definitions. --- src/theory/theory_preprocessor.cpp | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 3b68a33ca..f5e5fa505 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -350,30 +350,32 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term) { return (*find).second; } - unsigned nc = term.getNumChildren(); - if (nc == 0) + if (term.getNumChildren() == 0) { return preprocessWithProof(term); } Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; - - Node newTerm = term; + // We must rewrite before preprocessing, because some terms when rewritten + // may introduce new terms that are not top-level and require preprocessing. + // An example of this is (forall ((x Int)) (and (tail L) (P x))) which + // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L) + // must be preprocessed as a child here. + Node newTerm = rewriteWithProof(term); // do not rewrite inside quantifiers - if (!term.isClosure()) + if (newTerm.getNumChildren() > 0 && !newTerm.isClosure()) { - NodeBuilder<> newNode(term.getKind()); - if (term.getMetaKind() == kind::metakind::PARAMETERIZED) + NodeBuilder<> newNode(newTerm.getKind()); + if (newTerm.getMetaKind() == kind::metakind::PARAMETERIZED) { - newNode << term.getOperator(); + newNode << newTerm.getOperator(); } - unsigned i; - for (i = 0; i < nc; ++i) + for (const Node& nt : newTerm) { - newNode << ppTheoryRewrite(term[i]); + newNode << ppTheoryRewrite(nt); } newTerm = Node(newNode); + newTerm = rewriteWithProof(newTerm); } - newTerm = rewriteWithProof(newTerm); newTerm = preprocessWithProof(newTerm); d_ppCache[term] = newTerm; Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl; -- cgit v1.2.3 From c41a2e9be2422a211b9687833c97ba37485cd946 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Nov 2020 23:03:11 -0600 Subject: Fully decouple SmtEngine and the Expr layer (#5532) This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager. --- src/api/cvc4cpp.cpp | 2 +- src/expr/type.h | 2 +- src/smt/command.cpp | 4 +-- src/smt/smt_engine.cpp | 34 ++++++---------------- src/smt/smt_engine.h | 22 ++++++-------- src/theory/smt_engine_subsolver.cpp | 2 +- test/unit/expr/attribute_white.h | 2 +- test/unit/expr/type_node_white.h | 2 +- test/unit/preprocessing/pass_bv_gauss_white.h | 2 +- test/unit/prop/cnf_stream_white.h | 4 +-- test/unit/theory/evaluator_white.h | 2 +- test/unit/theory/sequences_rewriter_white.h | 5 ++-- test/unit/theory/theory_arith_white.h | 2 +- test/unit/theory/theory_bags_normal_form_white.h | 2 +- test/unit/theory/theory_bags_rewriter_white.h | 2 +- test/unit/theory/theory_bags_type_rules_white.h | 2 +- test/unit/theory/theory_bv_rewriter_white.h | 5 ++-- test/unit/theory/theory_bv_white.h | 2 +- test/unit/theory/theory_engine_white.h | 2 +- .../theory_quantifiers_bv_instantiator_white.h | 2 +- .../theory/theory_quantifiers_bv_inverter_white.h | 2 +- .../theory/theory_sets_type_enumerator_white.h | 2 +- test/unit/theory/theory_sets_type_rules_white.h | 2 +- .../theory/theory_strings_skolem_cache_black.h | 4 +-- test/unit/theory/theory_strings_word_white.h | 4 +-- test/unit/theory/theory_white.h | 2 +- test/unit/theory/type_enumerator_white.h | 2 +- 27 files changed, 49 insertions(+), 71 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 9b79b5c45..5eabcfe62 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3093,7 +3093,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const Solver::Solver(Options* opts) { d_exprMgr.reset(new ExprManager); - d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts)); + d_smtEngine.reset(new SmtEngine(d_exprMgr->getNodeManager(), opts)); d_smtEngine->setSolver(this); Options& o = d_smtEngine->getOptions(); d_rng.reset(new Random(o[options::seed])); diff --git a/src/expr/type.h b/src/expr/type.h index 69a8363dc..0b923f027 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -33,7 +33,7 @@ class Expr; class TypeNode; struct CVC4_PUBLIC ExprManagerMapCollection; -class CVC4_PUBLIC SmtEngine; +class SmtEngine; class CVC4_PUBLIC Datatype; class Record; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 154166eb7..fa3eb66c0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1442,8 +1442,8 @@ void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm) { solver->getSmtEngine()->setUserAttribute( d_attr, - d_term.getExpr(), - api::termVectorToExprs(d_termValues), + d_term.getNode(), + api::termVectorToNodes(d_termValues), d_strValue); } d_commandStatus = CommandSuccess::instance(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d623fdef..161c2eba6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -73,10 +73,9 @@ using namespace CVC4::theory; namespace CVC4 { -SmtEngine::SmtEngine(ExprManager* em, Options* optr) +SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_state(new SmtEngineState(*this)), - d_exprManager(em), - d_nodeManager(d_exprManager->getNodeManager()), + d_nodeManager(nm), d_absValues(new AbstractValues(d_nodeManager)), d_asserts(new Assertions(getUserContext(), *d_absValues.get())), d_dumpm(new DumpManager(getUserContext())), @@ -525,14 +524,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "all-statistics") { vector stats; - for (StatisticsRegistry::const_iterator i = - NodeManager::fromExprManager(d_exprManager) - ->getStatisticsRegistry() - ->begin(); - i - != NodeManager::fromExprManager(d_exprManager) - ->getStatisticsRegistry() - ->end(); + StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry(); + for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end(); ++i) { vector v; @@ -1637,7 +1630,6 @@ void SmtEngine::pop() { void SmtEngine::reset() { SmtScope smts(this); - ExprManager *em = d_exprManager; Trace("smt") << "SMT reset()" << endl; if(Dump.isOn("benchmark")) { getOutputManager().getPrinter().toStreamCmdReset( @@ -1647,7 +1639,7 @@ void SmtEngine::reset() Options opts; opts.copyValues(d_originalOptions); this->~SmtEngine(); - new (this) SmtEngine(em, &opts); + new (this) SmtEngine(d_nodeManager, &opts); // Restore data set after creation notifyStartParsing(filename); } @@ -1713,10 +1705,7 @@ unsigned long SmtEngine::getResourceRemaining() const return d_resourceManager->getResourceRemaining(); } -NodeManager* SmtEngine::getNodeManager() const -{ - return d_exprManager->getNodeManager(); -} +NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; } Statistics SmtEngine::getStatistics() const { @@ -1733,20 +1722,15 @@ void SmtEngine::safeFlushStatistics(int fd) const { } void SmtEngine::setUserAttribute(const std::string& attr, - Expr expr, - const std::vector& expr_values, + Node expr, + const std::vector& expr_values, const std::string& str_value) { SmtScope smts(this); finishInit(); - std::vector node_values; - for (std::size_t i = 0, n = expr_values.size(); i < n; i++) - { - node_values.push_back( expr_values[i].getNode() ); - } TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - te->setUserAttribute(attr, expr.getNode(), node_values, str_value); + te->setUserAttribute(attr, expr, expr_values, str_value); } void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1c83fa61f..a55428b55 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -21,13 +21,12 @@ #include #include +#include #include "base/modal_exception.h" #include "context/cdhashmap_forward.h" #include "context/cdhashset_forward.h" #include "context/cdlist_forward.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "options/options.h" #include "smt/logic_exception.h" #include "smt/output_manager.h" @@ -48,9 +47,10 @@ namespace CVC4 { template class NodeTemplate; typedef NodeTemplate Node; typedef NodeTemplate TNode; +class TypeNode; struct NodeHashFunction; -class SmtEngine; +class NodeManager; class DecisionEngine; class TheoryEngine; class ProofManager; @@ -58,6 +58,7 @@ class UnsatCore; class LogicRequest; class StatisticsRegistry; class Printer; +class ResourceManager; /* -------------------------------------------------------------------------- */ @@ -147,7 +148,7 @@ class CVC4_PUBLIC SmtEngine * If provided, optr is a pointer to a set of options that should initialize the values * of the options object owned by this class. */ - SmtEngine(ExprManager* em, Options* optr = nullptr); + SmtEngine(NodeManager* nm, Options* optr = nullptr); /** Destruct the SMT engine. */ ~SmtEngine(); @@ -691,7 +692,7 @@ class CVC4_PUBLIC SmtEngine /** * Completely reset the state of the solver, as though destroyed and * recreated. The result is as if newly constructed (so it still - * retains the same options structure and ExprManager). + * retains the same options structure and NodeManager). */ void reset(); @@ -785,9 +786,6 @@ class CVC4_PUBLIC SmtEngine */ unsigned long getResourceRemaining() const; - /** Permit access to the underlying ExprManager. */ - ExprManager* getExprManager() const { return d_exprManager; } - /** Permit access to the underlying NodeManager. */ NodeManager* getNodeManager() const; @@ -806,8 +804,8 @@ class CVC4_PUBLIC SmtEngine * In SMT-LIBv2 this is done via the syntax (! expr :attr) */ void setUserAttribute(const std::string& attr, - Expr expr, - const std::vector& expr_values, + Node expr, + const std::vector& expr_values, const std::string& str_value); /** Get the options object (const and non-const versions) */ @@ -1013,9 +1011,7 @@ class CVC4_PUBLIC SmtEngine */ std::unique_ptr d_state; - /** Our expression manager */ - ExprManager* d_exprManager; - /** Our internal expression/node manager */ + /** Our internal node manager */ NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index ed10e85ae..ee1ae198f 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -48,7 +48,7 @@ void initializeSubsolver(std::unique_ptr& smte, NodeManager* nm = NodeManager::currentNM(); SmtEngine* smtCurr = smt::currentSmtEngine(); // must copy the options - smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions())); + smte.reset(new SmtEngine(nm, &smtCurr->getOptions())); smte->setIsInternalSubsolver(); smte->setLogic(smtCurr->getLogicInfo()); // set the options diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index f1b782be2..de1795264 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -66,7 +66,7 @@ class AttributeWhite : public CxxTest::TestSuite { { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smtEngine = new SmtEngine(d_em); + d_smtEngine = new SmtEngine(d_nm); d_scope = new SmtScope(d_smtEngine); d_booleanType = new TypeNode(d_nm->booleanType()); } diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 22d3f0d84..8ac17bbbd 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -42,7 +42,7 @@ class TypeNodeWhite : public CxxTest::TestSuite { { d_em = new ExprManager(); d_nm = d_em->getNodeManager(); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new NodeManagerScope(d_nm); } diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index 0ff00a7d5..a0a708c5b 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -174,7 +174,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index ae79e1517..495097a79 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -131,9 +131,9 @@ class CnfStreamWhite : public CxxTest::TestSuite { void setUp() override { d_exprManager = new ExprManager(); - d_smt = new SmtEngine(d_exprManager); - d_smt->d_logic.lock(); d_nodeManager = NodeManager::fromExprManager(d_exprManager); + d_smt = new SmtEngine(d_nodeManager); + d_smt->d_logic.lock(); d_scope = new SmtScope(d_smt); // Notice that this unit test uses the theory engine of a created SMT diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index 421987e3c..1f33d0fbf 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -50,7 +50,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em, &opts); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index 1215b4a31..09cb925a3 100644 --- a/test/unit/theory/sequences_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -47,12 +47,11 @@ class SequencesRewriterWhite : public CxxTest::TestSuite Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; - d_smt = new SmtEngine(d_em, &opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); d_smt->finishInit(); d_rewriter = new ExtendedRewriter(true); - - d_nm = NodeManager::currentNM(); } void tearDown() override diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index f0b3f18fe..3475b1dc8 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -101,7 +101,7 @@ public: { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_smt->setOption("incremental", CVC4::SExpr(false)); d_ctxt = d_smt->getContext(); d_uctxt = d_smt->getUserContext(); diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h index 4e19ba90e..72fc4284e 100644 --- a/test/unit/theory/theory_bags_normal_form_white.h +++ b/test/unit/theory/theory_bags_normal_form_white.h @@ -35,8 +35,8 @@ class BagsNormalFormWhite : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); d_rewriter.reset(new BagsRewriter(nullptr)); } diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h index e47e32784..a58e2cdad 100644 --- a/test/unit/theory/theory_bags_rewriter_white.h +++ b/test/unit/theory/theory_bags_rewriter_white.h @@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); d_rewriter.reset(new BagsRewriter(nullptr)); } diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h index e454dfa28..8d1db858d 100644 --- a/test/unit/theory/theory_bags_type_rules_white.h +++ b/test/unit/theory/theory_bags_type_rules_white.h @@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index fae90918a..738a51831 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -41,11 +41,10 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; - d_smt = new SmtEngine(d_em, &opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); d_smt->finishInit(); - - d_nm = NodeManager::currentNM(); } void tearDown() override diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index bfde7866e..f568dc779 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -54,7 +54,7 @@ public: { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 8a99946e5..97da7eb8b 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -192,8 +192,8 @@ public: void setUp() override { d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_ctxt = d_smt->getContext(); diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index f2c5f0e1d..e19459f15 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -63,7 +63,7 @@ void BvInstantiatorWhite::setUp() { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index bb44656bc..ac25f60a9 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -222,7 +222,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_smt->setOption("cegqi-full", CVC4::SExpr(true)); d_smt->setOption("produce-models", CVC4::SExpr(true)); d_scope = new SmtScope(d_smt); diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index 965e59267..1b5ba1dcb 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -36,8 +36,8 @@ class SetEnumeratorWhite : public CxxTest::TestSuite void setUp() override { d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index 66c8dc123..00b012745 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -28,8 +28,8 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite { d_slv.reset(new Solver()); d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h index 4135adb0c..dd70dd5b9 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.h +++ b/test/unit/theory/theory_strings_skolem_cache_black.h @@ -35,13 +35,13 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); + d_nm = NodeManager::fromExprManager(d_em.get()); + d_smt.reset(new SmtEngine(d_nm)); d_scope.reset(new SmtScope(d_smt.get())); // Ensure that the SMT engine is fully initialized (required for the // rewriter) d_smt->push(); - d_nm = NodeManager::fromExprManager(d_em.get()); } void tearDown() override {} diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index 69143a69c..ce432d385 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -38,10 +38,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; - d_smt = new SmtEngine(d_em, &opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); - d_nm = NodeManager::currentNM(); } void tearDown() override diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 552aeb3c6..f69830fd8 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -175,7 +175,7 @@ class TheoryBlack : public CxxTest::TestSuite { { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_ctxt = d_smt->getContext(); d_uctxt = d_smt->getUserContext(); d_scope = new SmtScope(d_smt); diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index ea5a38913..24bf9922e 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -42,8 +42,8 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { void setUp() override { d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } -- cgit v1.2.3 From 70f0cddbce01fa17622b7b70b638794181aefec5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 26 Nov 2020 04:43:19 -0600 Subject: Move expand definitions to its own file (#5528) We are changing our policy on how expand definitions is handled during preprocessing. This will require some additions to expand definitions handling. This PR makes a standalone module for expanding definitions. --- src/CMakeLists.txt | 2 + src/smt/expand_definitions.cpp | 278 +++++++++++++++++++++++++++++++++++++++++ src/smt/expand_definitions.h | 76 +++++++++++ src/smt/preprocessor.cpp | 9 +- src/smt/preprocessor.h | 3 + src/smt/process_assertions.cpp | 234 +--------------------------------- src/smt/process_assertions.h | 17 +-- 7 files changed, 371 insertions(+), 248 deletions(-) create mode 100644 src/smt/expand_definitions.cpp create mode 100644 src/smt/expand_definitions.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 70cb68431..869699ac5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -219,6 +219,8 @@ libcvc4_add_sources( smt/dump.h smt/dump_manager.cpp smt/dump_manager.h + smt/expand_definitions.cpp + smt/expand_definitions.h smt/listeners.cpp smt/listeners.h smt/logic_exception.h diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp new file mode 100644 index 000000000..20c4f8ef6 --- /dev/null +++ b/src/smt/expand_definitions.cpp @@ -0,0 +1,278 @@ +/********************* */ +/*! \file expand_definitions.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of expand definitions for an SMT engine. + **/ + +#include "smt/expand_definitions.h" + +#include +#include + +#include "expr/node_manager_attributes.h" +#include "smt/defined_function.h" +#include "smt/smt_engine.h" +#include "theory/theory_engine.h" + +using namespace CVC4::preprocessing; +using namespace CVC4::theory; +using namespace CVC4::kind; + +namespace CVC4 { +namespace smt { + +ExpandDefs::ExpandDefs(SmtEngine& smt, + ResourceManager& rm, + SmtEngineStatistics& stats) + : d_smt(smt), d_resourceManager(rm), d_smtStats(stats) +{ +} + +ExpandDefs::~ExpandDefs() {} + +Node ExpandDefs::expandDefinitions( + TNode n, + std::unordered_map& cache, + bool expandOnly) +{ + NodeManager* nm = d_smt.getNodeManager(); + std::stack> worklist; + std::stack result; + worklist.push(std::make_tuple(Node(n), Node(n), false)); + // The worklist is made of triples, each is input / original node then the + // output / rewritten node and finally a flag tracking whether the children + // have been explored (i.e. if this is a downward or upward pass). + + do + { + d_resourceManager.spendResource(ResourceManager::Resource::PreprocessStep); + + // n is the input / original + // node is the output / result + Node node; + bool childrenPushed; + std::tie(n, node, childrenPushed) = worklist.top(); + worklist.pop(); + + // Working downwards + if (!childrenPushed) + { + Kind k = n.getKind(); + + // we can short circuit (variable) leaves + if (n.isVar()) + { + SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); + SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n); + if (i != dfuns->end()) + { + Node f = (*i).second.getFormula(); + // must expand its definition + Node fe = expandDefinitions(f, cache, expandOnly); + // replacement must be closed + if ((*i).second.getFormals().size() > 0) + { + result.push( + nm->mkNode(LAMBDA, + nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()), + fe)); + continue; + } + // don't bother putting in the cache + result.push(fe); + continue; + } + // don't bother putting in the cache + result.push(n); + continue; + } + + // maybe it's in the cache + std::unordered_map::iterator cacheHit = + cache.find(n); + if (cacheHit != cache.end()) + { + TNode ret = (*cacheHit).second; + result.push(ret.isNull() ? n : ret); + continue; + } + + // otherwise expand it + bool doExpand = false; + if (k == APPLY_UF) + { + // Always do beta-reduction here. The reason is that there may be + // operators such as INTS_MODULUS in the body of the lambda that would + // otherwise be introduced by beta-reduction via the rewriter, but are + // not expanded here since the traversal in this function does not + // traverse the operators of nodes. Hence, we beta-reduce here to + // ensure terms in the body of the lambda are expanded during this + // call. + if (n.getOperator().getKind() == LAMBDA) + { + doExpand = true; + } + else + { + // We always check if this operator corresponds to a defined function. + doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); + } + } + if (doExpand) + { + std::vector formals; + TNode fm; + if (n.getOperator().getKind() == LAMBDA) + { + TNode op = n.getOperator(); + // lambda + for (unsigned i = 0; i < op[0].getNumChildren(); i++) + { + formals.push_back(op[0][i]); + } + fm = op[1]; + } + else + { + // application of a user-defined symbol + TNode func = n.getOperator(); + SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); + SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); + if (i == dfuns->end()) + { + throw TypeCheckingException( + n.toExpr(), + std::string("Undefined function: `") + func.toString() + "'"); + } + DefinedFunction def = (*i).second; + formals = def.getFormals(); + + if (Debug.isOn("expand")) + { + Debug("expand") << "found: " << n << std::endl; + Debug("expand") << " func: " << func << std::endl; + std::string name = func.getAttribute(expr::VarNameAttr()); + Debug("expand") << " : \"" << name << "\"" << std::endl; + } + if (Debug.isOn("expand")) + { + Debug("expand") << " defn: " << def.getFunction() << std::endl + << " ["; + if (formals.size() > 0) + { + copy(formals.begin(), + formals.end() - 1, + std::ostream_iterator(Debug("expand"), ", ")); + Debug("expand") << formals.back(); + } + Debug("expand") + << "]" << std::endl + << " " << def.getFunction().getType() << std::endl + << " " << def.getFormula() << std::endl; + } + + fm = def.getFormula(); + } + + Node instance = fm.substitute(formals.begin(), + formals.end(), + n.begin(), + n.begin() + formals.size()); + Debug("expand") << "made : " << instance << std::endl; + + Node expanded = expandDefinitions(instance, cache, expandOnly); + cache[n] = (n == expanded ? Node::null() : expanded); + result.push(expanded); + continue; + } + else if (!expandOnly) + { + // do not do any theory stuff if expandOnly is true + + theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node); + + Assert(t != NULL); + TrustNode trn = t->expandDefinition(n); + node = trn.isNull() ? Node(n) : trn.getNode(); + } + + // the partial functions can fall through, in which case we still + // consider their children + worklist.push(std::make_tuple( + Node(n), node, true)); // Original and rewritten result + + for (size_t i = 0; i < node.getNumChildren(); ++i) + { + worklist.push( + std::make_tuple(node[i], + node[i], + false)); // Rewrite the children of the result only + } + } + else + { + // Working upwards + // Reconstruct the node from it's (now rewritten) children on the stack + + Debug("expand") << "cons : " << node << std::endl; + if (node.getNumChildren() > 0) + { + // cout << "cons : " << node << std::endl; + NodeBuilder<> nb(node.getKind()); + if (node.getMetaKind() == metakind::PARAMETERIZED) + { + Debug("expand") << "op : " << node.getOperator() << std::endl; + // cout << "op : " << node.getOperator() << std::endl; + nb << node.getOperator(); + } + for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i) + { + Assert(!result.empty()); + Node expanded = result.top(); + result.pop(); + // cout << "exchld : " << expanded << std::endl; + Debug("expand") << "exchld : " << expanded << std::endl; + nb << expanded; + } + node = nb; + } + // Only cache once all subterms are expanded + cache[n] = n == node ? Node::null() : node; + result.push(node); + } + } while (!worklist.empty()); + + AlwaysAssert(result.size() == 1); + + return result.top(); +} + +void ExpandDefs::expandAssertions(AssertionPipeline& assertions, + bool expandOnly) +{ + Chat() << "expanding definitions in assertions..." << std::endl; + Trace("simplify") << "ExpandDefs::simplify(): expanding definitions" + << std::endl; + TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); + std::unordered_map cache; + for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) + { + Node assert = assertions[i]; + Node expd = expandDefinitions(assert, cache, expandOnly); + if (expd != assert) + { + assertions.replace(i, expd); + } + } +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h new file mode 100644 index 000000000..f40ee4a4e --- /dev/null +++ b/src/smt/expand_definitions.h @@ -0,0 +1,76 @@ +/********************* */ +/*! \file process_assertions.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The module for processing assertions for an SMT engine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__EXPAND_DEFINITIONS_H +#define CVC4__SMT__EXPAND_DEFINITIONS_H + +#include + +#include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" +#include "smt/smt_engine_stats.h" +#include "util/resource_manager.h" + +namespace CVC4 { + +class SmtEngine; + +namespace smt { + +/** + * Module in charge of expanding definitions for an SMT engine. + * + * Its main features is expandDefinitions(TNode, ...), which returns the + * expanded formula of a term. + */ +class ExpandDefs +{ + public: + ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats); + ~ExpandDefs(); + /** + * Expand definitions in term n. Return the expanded form of n. + * + * @param n The node to expand + * @param cache Cache of previous results + * @param expandOnly if true, then the expandDefinitions function of + * TheoryEngine is not called on subterms of n. + * @return The expanded term. + */ + Node expandDefinitions( + TNode n, + std::unordered_map& cache, + bool expandOnly = false); + /** + * Expand defintitions in assertions. This applies this above method to each + * assertion in the given pipeline. + */ + void expandAssertions(preprocessing::AssertionPipeline& assertions, + bool expandOnly = false); + + private: + /** Reference to the SMT engine */ + SmtEngine& d_smt; + /** Reference to resource manager */ + ResourceManager& d_resourceManager; + /** Reference to the SMT stats */ + SmtEngineStatistics& d_smtStats; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 5a1ce63a4..2c8592657 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -36,7 +36,8 @@ Preprocessor::Preprocessor(SmtEngine& smt, d_absValues(abs), d_propagator(true, true), d_assertionsProcessed(u, false), - d_processor(smt, *smt.getResourceManager(), stats), + d_exDefs(smt, *smt.getResourceManager(), stats), + d_processor(smt, d_exDefs, *smt.getResourceManager(), stats), d_rtf(u), d_pnm(nullptr) { @@ -108,7 +109,7 @@ RemoveTermFormulas& Preprocessor::getTermFormulaRemover() { return d_rtf; } Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly) { std::unordered_map cache; - return expandDefinitions(n, cache, expandOnly); + return d_exDefs.expandDefinitions(n, cache, expandOnly); } Node Preprocessor::expandDefinitions( @@ -125,7 +126,7 @@ Node Preprocessor::expandDefinitions( n.getType(true); } // expand only = true - return d_processor.expandDefinitions(n, cache, expandOnly); + return d_exDefs.expandDefinitions(n, cache, expandOnly); } Node Preprocessor::simplify(const Node& node, bool removeItes) @@ -143,7 +144,7 @@ Node Preprocessor::simplify(const Node& node, bool removeItes) nas.getType(true); } std::unordered_map cache; - Node n = d_processor.expandDefinitions(nas, cache); + Node n = d_exDefs.expandDefinitions(nas, cache); TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n); Node ns = ts.isNull() ? n : ts.getNode(); if (removeItes) diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index cb83f969e..220a433fe 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -20,6 +20,7 @@ #include #include "preprocessing/preprocessing_pass_context.h" +#include "smt/expand_definitions.h" #include "smt/process_assertions.h" #include "smt/term_formula_removal.h" #include "theory/booleans/circuit_propagator.h" @@ -125,6 +126,8 @@ class Preprocessor context::CDO d_assertionsProcessed; /** The preprocessing pass context */ std::unique_ptr d_ppContext; + /** Expand definitions module, responsible for expanding definitions */ + ExpandDefs d_exDefs; /** * Process assertions module, responsible for implementing the preprocessing * passes. diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 2011e7b83..c68b73336 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -53,9 +53,11 @@ class ScopeCounter }; ProcessAssertions::ProcessAssertions(SmtEngine& smt, + ExpandDefs& exDefs, ResourceManager& rm, SmtEngineStatistics& stats) : d_smt(smt), + d_exDefs(exDefs), d_resourceManager(rm), d_smtStats(stats), d_preprocessingPassContext(nullptr) @@ -128,21 +130,7 @@ bool ProcessAssertions::apply(Assertions& as) << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; dumpAssertions("pre-definition-expansion", assertions); - { - Chat() << "expanding definitions..." << endl; - Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions" - << endl; - TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); - unordered_map cache; - for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) - { - Node expd = expandDefinitions(assertions[i], cache); - if (expd != assertions[i]) - { - assertions.replace(i, expd); - } - } - } + d_exDefs.expandAssertions(assertions, false); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; @@ -550,222 +538,6 @@ void ProcessAssertions::dumpAssertions(const char* key, } } -Node ProcessAssertions::expandDefinitions( - TNode n, - unordered_map& cache, - bool expandOnly) -{ - NodeManager* nm = d_smt.getNodeManager(); - std::stack> worklist; - std::stack result; - worklist.push(std::make_tuple(Node(n), Node(n), false)); - // The worklist is made of triples, each is input / original node then the - // output / rewritten node and finally a flag tracking whether the children - // have been explored (i.e. if this is a downward or upward pass). - - do - { - spendResource(ResourceManager::Resource::PreprocessStep); - - // n is the input / original - // node is the output / result - Node node; - bool childrenPushed; - std::tie(n, node, childrenPushed) = worklist.top(); - worklist.pop(); - - // Working downwards - if (!childrenPushed) - { - Kind k = n.getKind(); - - // we can short circuit (variable) leaves - if (n.isVar()) - { - SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); - SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n); - if (i != dfuns->end()) - { - Node f = (*i).second.getFormula(); - // must expand its definition - Node fe = expandDefinitions(f, cache, expandOnly); - // replacement must be closed - if ((*i).second.getFormals().size() > 0) - { - result.push( - nm->mkNode(LAMBDA, - nm->mkNode(BOUND_VAR_LIST, (*i).second.getFormals()), - fe)); - continue; - } - // don't bother putting in the cache - result.push(fe); - continue; - } - // don't bother putting in the cache - result.push(n); - continue; - } - - // maybe it's in the cache - unordered_map::iterator cacheHit = - cache.find(n); - if (cacheHit != cache.end()) - { - TNode ret = (*cacheHit).second; - result.push(ret.isNull() ? n : ret); - continue; - } - - // otherwise expand it - bool doExpand = false; - if (k == APPLY_UF) - { - // Always do beta-reduction here. The reason is that there may be - // operators such as INTS_MODULUS in the body of the lambda that would - // otherwise be introduced by beta-reduction via the rewriter, but are - // not expanded here since the traversal in this function does not - // traverse the operators of nodes. Hence, we beta-reduce here to - // ensure terms in the body of the lambda are expanded during this - // call. - if (n.getOperator().getKind() == LAMBDA) - { - doExpand = true; - } - else - { - // We always check if this operator corresponds to a defined function. - doExpand = d_smt.isDefinedFunction(n.getOperator().toExpr()); - } - } - if (doExpand) - { - vector formals; - TNode fm; - if (n.getOperator().getKind() == LAMBDA) - { - TNode op = n.getOperator(); - // lambda - for (unsigned i = 0; i < op[0].getNumChildren(); i++) - { - formals.push_back(op[0][i]); - } - fm = op[1]; - } - else - { - // application of a user-defined symbol - TNode func = n.getOperator(); - SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); - SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); - if (i == dfuns->end()) - { - throw TypeCheckingException( - n.toExpr(), - string("Undefined function: `") + func.toString() + "'"); - } - DefinedFunction def = (*i).second; - formals = def.getFormals(); - - if (Debug.isOn("expand")) - { - Debug("expand") << "found: " << n << endl; - Debug("expand") << " func: " << func << endl; - string name = func.getAttribute(expr::VarNameAttr()); - Debug("expand") << " : \"" << name << "\"" << endl; - } - if (Debug.isOn("expand")) - { - Debug("expand") << " defn: " << def.getFunction() << endl - << " ["; - if (formals.size() > 0) - { - copy(formals.begin(), - formals.end() - 1, - ostream_iterator(Debug("expand"), ", ")); - Debug("expand") << formals.back(); - } - Debug("expand") << "]" << endl - << " " << def.getFunction().getType() << endl - << " " << def.getFormula() << endl; - } - - fm = def.getFormula(); - } - - Node instance = fm.substitute(formals.begin(), - formals.end(), - n.begin(), - n.begin() + formals.size()); - Debug("expand") << "made : " << instance << endl; - - Node expanded = expandDefinitions(instance, cache, expandOnly); - cache[n] = (n == expanded ? Node::null() : expanded); - result.push(expanded); - continue; - } - else if (!expandOnly) - { - // do not do any theory stuff if expandOnly is true - - theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node); - - Assert(t != NULL); - TrustNode trn = t->expandDefinition(n); - node = trn.isNull() ? Node(n) : trn.getNode(); - } - - // the partial functions can fall through, in which case we still - // consider their children - worklist.push(std::make_tuple( - Node(n), node, true)); // Original and rewritten result - - for (size_t i = 0; i < node.getNumChildren(); ++i) - { - worklist.push( - std::make_tuple(node[i], - node[i], - false)); // Rewrite the children of the result only - } - } - else - { - // Working upwards - // Reconstruct the node from it's (now rewritten) children on the stack - - Debug("expand") << "cons : " << node << endl; - if (node.getNumChildren() > 0) - { - // cout << "cons : " << node << endl; - NodeBuilder<> nb(node.getKind()); - if (node.getMetaKind() == metakind::PARAMETERIZED) - { - Debug("expand") << "op : " << node.getOperator() << endl; - // cout << "op : " << node.getOperator() << endl; - nb << node.getOperator(); - } - for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; ++i) - { - Assert(!result.empty()); - Node expanded = result.top(); - result.pop(); - // cout << "exchld : " << expanded << endl; - Debug("expand") << "exchld : " << expanded << endl; - nb << expanded; - } - node = nb; - } - // Only cache once all subterms are expanded - cache[n] = n == node ? Node::null() : node; - result.push(node); - } - } while (!worklist.empty()); - - AlwaysAssert(result.size() == 1); - - return result.top(); -} - void ProcessAssertions::collectSkolems( IteSkolemMap& iskMap, TNode n, diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index d260edf14..072603e7d 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -26,6 +26,7 @@ #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/assertions.h" +#include "smt/expand_definitions.h" #include "smt/smt_engine_stats.h" #include "util/resource_manager.h" @@ -53,11 +54,11 @@ class ProcessAssertions { /** The types for the recursive function definitions */ typedef context::CDList NodeList; - typedef unordered_map NodeToNodeHashMap; typedef unordered_map NodeToBoolHashMap; public: ProcessAssertions(SmtEngine& smt, + ExpandDefs& exDefs, ResourceManager& rm, SmtEngineStatistics& stats); ~ProcessAssertions(); @@ -76,22 +77,12 @@ class ProcessAssertions * processing the assertions. */ bool apply(Assertions& as); - /** - * Expand definitions in term n. Return the expanded form of n. - * - * @param n The node to expand - * @param cache Cache of previous results - * @param expandOnly if true, then the expandDefinitions function of - * TheoryEngine is not called on subterms of n. - * @return The expanded term. - */ - Node expandDefinitions(TNode n, - NodeToNodeHashMap& cache, - bool expandOnly = false); private: /** Reference to the SMT engine */ SmtEngine& d_smt; + /** Reference to expand definitions module */ + ExpandDefs& d_exDefs; /** Reference to resource manager */ ResourceManager& d_resourceManager; /** Reference to the SMT stats */ -- cgit v1.2.3 From d3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 26 Nov 2020 09:15:30 -0600 Subject: Removing infrastructure related to SMT model (#5527) Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine. The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener. --- src/smt/check_models.cpp | 14 ++------- src/smt/command.cpp | 17 +---------- src/smt/command.h | 5 ---- src/smt/dump_manager.cpp | 76 ++++-------------------------------------------- src/smt/dump_manager.h | 30 +------------------ src/smt/model.cpp | 14 +-------- src/smt/model.h | 13 +-------- src/smt/node_command.cpp | 20 +------------ src/smt/node_command.h | 5 ---- src/smt/smt_engine.cpp | 2 +- 10 files changed, 13 insertions(+), 183 deletions(-) diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 612084de2..56d54eec9 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -67,24 +67,14 @@ void CheckModels::checkModel(Model* m, /* substituteUnderQuantifiers = */ false); Trace("check-model") << "checkModel: Collect substitution..." << std::endl; - for (size_t k = 0, ncmd = m->getNumCommands(); k < ncmd; ++k) + const std::vector& decTerms = m->getDeclaredTerms(); + for (const Node& func : decTerms) { - const DeclareFunctionNodeCommand* c = - dynamic_cast(m->getCommand(k)); - Notice() << "SmtEngine::checkModel(): model command " << k << " : " - << m->getCommand(k)->toString() << std::endl; - if (c == nullptr) - { - // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... - Notice() << "SmtEngine::checkModel(): skipping..." << std::endl; - continue; - } // We have a DECLARE-FUN: // // We'll first do some checks, then add to our substitution map // the mapping: function symbol |-> value - Node func = c->getFunction(); Node val = m->getValue(func); Notice() << "SmtEngine::checkModel(): adding substitution: " << func diff --git a/src/smt/command.cpp b/src/smt/command.cpp index fa3eb66c0..e6361be9e 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1069,25 +1069,12 @@ DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, api::Sort sort) : DeclarationDefinitionCommand(id), d_func(func), - d_sort(sort), - d_printInModel(true), - d_printInModelSetByUser(false) + d_sort(sort) { } api::Term DeclareFunctionCommand::getFunction() const { return d_func; } api::Sort DeclareFunctionCommand::getSort() const { return d_sort; } -bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; } -bool DeclareFunctionCommand::getPrintInModelSetByUser() const -{ - return d_printInModelSetByUser; -} - -void DeclareFunctionCommand::setPrintInModel(bool p) -{ - d_printInModel = p; - d_printInModelSetByUser = true; -} void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { @@ -1100,8 +1087,6 @@ Command* DeclareFunctionCommand::clone() const { DeclareFunctionCommand* dfc = new DeclareFunctionCommand(d_symbol, d_func, d_sort); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; return dfc; } diff --git a/src/smt/command.h b/src/smt/command.h index 96a6938d6..0b86f3539 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -387,16 +387,11 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand protected: api::Term d_func; api::Sort d_sort; - bool d_printInModel; - bool d_printInModelSetByUser; public: DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort); api::Term getFunction() const; api::Sort getSort() const; - bool getPrintInModel() const; - bool getPrintInModelSetByUser() const; - void setPrintInModel(bool p); void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 9b7fba5a2..9d3031b4d 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -24,8 +24,6 @@ namespace smt { DumpManager::DumpManager(context::UserContext* u) : d_fullyInited(false), - d_modelGlobalCommands(), - d_modelCommands(u), d_dumpCommands() { } @@ -33,8 +31,6 @@ DumpManager::DumpManager(context::UserContext* u) DumpManager::~DumpManager() { d_dumpCommands.clear(); - d_modelCommandsAlloc.clear(); - d_modelGlobalCommands.clear(); } void DumpManager::finishInit() @@ -49,8 +45,10 @@ void DumpManager::finishInit() d_fullyInited = true; } - -void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); } +void DumpManager::resetAssertions() +{ + // currently, do nothing +} void DumpManager::addToModelCommandAndDump(const NodeCommand& c, uint32_t flags, @@ -58,29 +56,6 @@ void DumpManager::addToModelCommandAndDump(const NodeCommand& c, const char* dumpTag) { Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << std::endl; - // If we aren't yet fully inited, the user might still turn on - // produce-models. So let's keep any commands around just in - // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares - // sort "U" in QF_UF before setLogic() is run and we still want to - // support finding card(U) with --finite-model-find, and (2) to - // decouple SmtEngine and ExprManager if the user does a few - // ExprManager::mkSort() before SmtEngine::setOption("produce-models") - // and expects to find their cardinalities in the model. - if ((!d_fullyInited || options::produceModels()) - && (flags & ExprManager::VAR_FLAG_DEFINED) == 0) - { - if (flags & ExprManager::VAR_FLAG_GLOBAL) - { - d_modelGlobalCommands.push_back(std::unique_ptr(c.clone())); - } - else - { - NodeCommand* cc = c.clone(); - d_modelCommands.push_back(cc); - // also remember for memory management purposes - d_modelCommandsAlloc.push_back(std::unique_ptr(cc)); - } - } if (Dump.isOn(dumpTag)) { if (d_fullyInited) @@ -97,48 +72,7 @@ void DumpManager::addToModelCommandAndDump(const NodeCommand& c, void DumpManager::setPrintFuncInModel(Node f, bool p) { Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; - for (std::unique_ptr& c : d_modelGlobalCommands) - { - DeclareFunctionNodeCommand* dfc = - dynamic_cast(c.get()); - if (dfc != NULL) - { - Node df = dfc->getFunction(); - if (df == f) - { - dfc->setPrintInModel(p); - } - } - } - for (NodeCommand* c : d_modelCommands) - { - DeclareFunctionNodeCommand* dfc = - dynamic_cast(c); - if (dfc != NULL) - { - Node df = dfc->getFunction(); - if (df == f) - { - dfc->setPrintInModel(p); - } - } - } -} - -size_t DumpManager::getNumModelCommands() const -{ - return d_modelCommands.size() + d_modelGlobalCommands.size(); -} - -const NodeCommand* DumpManager::getModelCommand(size_t i) const -{ - Assert(i < getNumModelCommands()); - // index the global commands first, then the locals - if (i < d_modelGlobalCommands.size()) - { - return d_modelGlobalCommands[i].get(); - } - return d_modelCommands[i - d_modelGlobalCommands.size()]; + // TODO (cvc4-wishues/issues/75): implement } } // namespace smt diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 0ba8e0b8b..eaedf39a1 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -31,14 +31,10 @@ namespace smt { /** * This utility is responsible for: - * (1) storing information required for SMT-LIB queries such as get-model, - * which requires knowing what symbols are declared and should be printed in - * the model. - * (2) implementing some dumping traces e.g. --dump=declarations. + * implementing some dumping traces e.g. --dump=declarations. */ class DumpManager { - typedef context::CDList CommandList; public: DumpManager(context::UserContext* u); @@ -65,34 +61,10 @@ class DumpManager * Set that function f should print in the model if and only if p is true. */ void setPrintFuncInModel(Node f, bool p); - /** get number of commands to report in a model */ - size_t getNumModelCommands() const; - /** get model command at index i */ - const NodeCommand* getModelCommand(size_t i) const; private: /** Fully inited */ bool d_fullyInited; - - /** - * A list of commands that should be in the Model globally (i.e., - * regardless of push/pop). Only maintained if produce-models option - * is on. - */ - std::vector> d_modelGlobalCommands; - - /** - * A list of commands that should be in the Model locally (i.e., - * it is context-dependent on push/pop). Only maintained if - * produce-models option is on. - */ - CommandList d_modelCommands; - /** - * A list of model commands allocated to d_modelCommands at any time. This - * is maintained for memory management purposes. - */ - std::vector> d_modelCommandsAlloc; - /** * A vector of declaration commands waiting to be dumped out. * Once the SmtEngine is fully initialized, we'll dump them. diff --git a/src/smt/model.cpp b/src/smt/model.cpp index b734ad9e9..8a9f944d2 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -26,29 +26,17 @@ namespace CVC4 { namespace smt { -Model::Model(SmtEngine& smt, theory::TheoryModel* tm) - : d_smt(smt), d_isKnownSat(false), d_tmodel(tm) +Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm) { Assert(d_tmodel != nullptr); } std::ostream& operator<<(std::ostream& out, const Model& m) { - smt::SmtScope smts(&m.d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, m); return out; } -size_t Model::getNumCommands() const -{ - return d_smt.getDumpManager()->getNumModelCommands(); -} - -const NodeCommand* Model::getCommand(size_t i) const -{ - return d_smt.getDumpManager()->getModelCommand(i); -} - theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; } const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; } diff --git a/src/smt/model.h b/src/smt/model.h index 0913922d1..18675040a 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -27,7 +27,6 @@ namespace CVC4 { class SmtEngine; -class NodeCommand; namespace smt { @@ -49,13 +48,9 @@ class Model { public: /** construct */ - Model(SmtEngine& smt, theory::TheoryModel* tm); + Model(theory::TheoryModel* tm); /** virtual destructor */ ~Model() {} - /** get the smt engine that this model is hooked up to */ - SmtEngine* getSmtEngine() { return &d_smt; } - /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ - const SmtEngine* getSmtEngine() const { return &d_smt; } /** get the input name (file name, etc.) this model is associated to */ std::string getInputName() const { return d_inputName; } /** @@ -77,10 +72,6 @@ class Model { /** Does this model have approximations? */ bool hasApproximations() const; //----------------------- end helper methods - /** get number of commands to report */ - size_t getNumCommands() const; - /** get command */ - const NodeCommand* getCommand(size_t i) const; //----------------------- model declarations /** Clear the current model declarations. */ void clearModelDeclarations(); @@ -100,8 +91,6 @@ class Model { const std::vector& getDeclaredTerms() const; //----------------------- end model declarations protected: - /** The SmtEngine we're associated with */ - SmtEngine& d_smt; /** the input name (file name, etc.) this model is associated to */ std::string d_inputName; /** diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 91184d27d..815f99132 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -51,9 +51,7 @@ DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id, TypeNode type) : d_id(id), d_fun(expr), - d_type(type), - d_printInModel(true), - d_printInModelSetByUser(false) + d_type(type) { } @@ -72,22 +70,6 @@ NodeCommand* DeclareFunctionNodeCommand::clone() const const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; } -bool DeclareFunctionNodeCommand::getPrintInModel() const -{ - return d_printInModel; -} - -bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const -{ - return d_printInModelSetByUser; -} - -void DeclareFunctionNodeCommand::setPrintInModel(bool p) -{ - d_printInModel = p; - d_printInModelSetByUser = true; -} - /* -------------------------------------------------------------------------- */ /* class DeclareTypeNodeCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/node_command.h b/src/smt/node_command.h index 8cf9a5e10..e1a15e62c 100644 --- a/src/smt/node_command.h +++ b/src/smt/node_command.h @@ -68,16 +68,11 @@ class DeclareFunctionNodeCommand : public NodeCommand OutputLanguage language = language::output::LANG_AUTO) const override; NodeCommand* clone() const override; const Node& getFunction() const; - bool getPrintInModel() const; - bool getPrintInModelSetByUser() const; - void setPrintInModel(bool p); private: std::string d_id; Node d_fun; TypeNode d_type; - bool d_printInModel; - bool d_printInModelSetByUser; }; /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 161c2eba6..0f40db530 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -243,7 +243,7 @@ void SmtEngine::finishInit() TheoryModel* tm = te->getModel(); if (tm != nullptr) { - d_model.reset(new Model(*this, tm)); + d_model.reset(new Model(tm)); // make the check models utility d_checkModels.reset(new CheckModels(*d_smtSolver.get())); } -- cgit v1.2.3 From 865d1ee48de8e4a21d1e97c707be46c34918367d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 26 Nov 2020 17:02:16 +0100 Subject: Make CAD solver work for empty set of assertions (#5535) When called with no assertions, the CAD solver would still go to work and then segfault when trying to access the first variable. This PR adds an explicit check for this case and adds a regression. Fixes #5534 . --- src/theory/arith/nl/cad_solver.cpp | 8 ++++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/issue5534-no-assertions.smt2 | 12 ++++++++++++ 3 files changed, 21 insertions(+) create mode 100644 test/regress/regress0/nl/issue5534-no-assertions.smt2 diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 831530995..ea0739235 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -71,6 +71,10 @@ void CadSolver::initLastCall(const std::vector& assertions) void CadSolver::checkFull() { #ifdef CVC4_POLY_IMP + if (d_CAC.getConstraints().getConstraints().empty()) { + Trace("nl-cad") << "No constraints. Return." << std::endl; + return; + } auto covering = d_CAC.getUnsatCover(); if (covering.empty()) { @@ -101,6 +105,10 @@ void CadSolver::checkFull() void CadSolver::checkPartial() { #ifdef CVC4_POLY_IMP + if (d_CAC.getConstraints().getConstraints().empty()) { + Trace("nl-cad") << "No constraints. Return." << std::endl; + return; + } auto covering = d_CAC.getUnsatCover(0, true); if (covering.empty()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8969b6c01..816202fa9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -622,6 +622,7 @@ set(regress_0_tests regress0/nl/issue3971.smt2 regress0/nl/issue3991.smt2 regress0/nl/issue4007-rint-uf.smt2 + regress0/nl/issue5534-no-assertions.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 diff --git a/test/regress/regress0/nl/issue5534-no-assertions.smt2 b/test/regress/regress0/nl/issue5534-no-assertions.smt2 new file mode 100644 index 000000000..e7a9f0cd1 --- /dev/null +++ b/test/regress/regress0/nl/issue5534-no-assertions.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +(set-logic QF_UFNRA) +(declare-fun r () Real) +(declare-fun u (Real Real) Bool) +(assert (u 0.0 (* r r))) +(push) +(assert (and (< r 0.0) (< 0.0 r))) +(check-sat) +(pop) +(check-sat) \ No newline at end of file -- cgit v1.2.3