diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-14 17:09:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-14 17:09:59 -0600 |
commit | 528e801343c692b0ce8123f8754e069e6523f5dc (patch) | |
tree | 517c86381e7a0535c376d244c830365d04e3aa62 /src | |
parent | 08289dd911aff28110baf0fd815fd912f8b76fd3 (diff) |
Remove quantifiers rewrite rules infrastructure (#3754)
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 8 | ||||
-rw-r--r-- | src/bindings/java/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/options/quantifiers_options.toml | 9 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 95 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 27 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 18 | ||||
-rw-r--r-- | src/smt/command.cpp | 247 | ||||
-rw-r--r-- | src/smt/command.h | 74 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/kinds | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 40 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 133 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 309 | ||||
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.h | 86 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers_type_rules.h | 85 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 21 | ||||
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 4 |
20 files changed, 25 insertions, 1175 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 975dd26f6..871cb2f99 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -544,8 +544,6 @@ libcvc4_add_sources( theory/quantifiers/query_generator.h theory/quantifiers/relevant_domain.cpp theory/quantifiers/relevant_domain.h - theory/quantifiers/rewrite_engine.cpp - theory/quantifiers/rewrite_engine.h theory/quantifiers/single_inv_partition.cpp theory/quantifiers/single_inv_partition.h theory/quantifiers/skolemize.cpp diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index bb2700706..2242c8e00 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2181,14 +2181,6 @@ enum CVC4_PUBLIC Kind : int32_t INST_PATTERN_LIST, /* predicate for specifying term in instantiation closure. */ INST_CLOSURE, - /* general rewrite rule (for rewrite-rules theory) */ - REWRITE_RULE, - /* actual rewrite rule (for rewrite-rules theory) */ - RR_REWRITE, - /* actual reduction rule (for rewrite-rules theory) */ - RR_REDUCTION, - /* actual deduction rule (for rewrite-rules theory) */ - RR_DEDUCTION, /* Sort Kinds ------------------------------------------------------------ */ diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 3cd6a7e51..7c2985e5c 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -160,7 +160,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/PopCommand.java ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java ${CMAKE_CURRENT_BINARY_DIR}/Proof.java - ${CMAKE_CURRENT_BINARY_DIR}/PropagateRuleCommand.java ${CMAKE_CURRENT_BINARY_DIR}/PushCommand.java ${CMAKE_CURRENT_BINARY_DIR}/QueryCommand.java ${CMAKE_CURRENT_BINARY_DIR}/QuitCommand.java @@ -177,7 +176,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/ResetCommand.java ${CMAKE_CURRENT_BINARY_DIR}/ResourceManager.java ${CMAKE_CURRENT_BINARY_DIR}/Result.java - ${CMAKE_CURRENT_BINARY_DIR}/RewriteRuleCommand.java ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 908846bea..84545e66e 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -899,15 +899,6 @@ header = "options/quantifiers_options.h" ### Rewrite rules options [[option]] - name = "quantRewriteRules" - category = "regular" - long = "rewrite-rules" - type = "bool" - default = "false" - read_only = true - help = "use rewrite rules module" - -[[option]] name = "rrOneInstPerRound" category = "regular" long = "rr-one-inst-per-round" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index aed62f94c..90303dd40 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1254,8 +1254,6 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] - | rewriterulesCommand[cmd] - /* Support some of Z3's extended SMT-LIB commands */ | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1545,43 +1543,6 @@ datatypesDef[bool isCo, } ; -rewriterulesCommand[std::unique_ptr<CVC4::Command>* cmd] -@declarations { - std::vector<Expr> guards, heads, triggers; - Expr head, body, bvl, expr, expr2; - Kind kind; -} - : /* rewrite rules */ - REWRITE_RULE_TOK { kind = CVC4::kind::RR_REWRITE; } - { PARSER_STATE->pushScope(true); } - boundVarList[bvl] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK - LPAREN_TOK (termList[guards,expr])? RPAREN_TOK - term[head, expr2] - term[body, expr2] - { - *cmd = PARSER_STATE->assertRewriteRule( - kind, bvl, triggers, guards, {head}, body); - } - /* propagation rule */ - | rewritePropaKind[kind] - { PARSER_STATE->pushScope(true); } - boundVarList[bvl] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK - LPAREN_TOK (termList[guards,expr])? RPAREN_TOK - LPAREN_TOK (termList[heads,expr])? RPAREN_TOK - term[body, expr2] - { - *cmd = PARSER_STATE->assertRewriteRule( - kind, bvl, triggers, guards, heads, body); - } - ; - -rewritePropaKind[CVC4::Kind& kind] - : REDUCTION_RULE_TOK { $kind = CVC4::kind::RR_REDUCTION; } - | PROPAGATION_RULE_TOK { $kind = CVC4::kind::RR_DEDUCTION; } - ; - pattern[CVC4::Expr& expr] @declarations { std::vector<Expr> patexpr; @@ -1631,8 +1592,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK - | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK - | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) + | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK) { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } ; @@ -1713,25 +1673,11 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] args.push_back(bvl); PARSER_STATE->popScope(); - switch(f.getKind()) { - case CVC4::kind::RR_REWRITE: - case CVC4::kind::RR_REDUCTION: - case CVC4::kind::RR_DEDUCTION: - if(kind == CVC4::kind::EXISTS) { - PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite " - "rule."); - } - args.push_back(f2); // guards - args.push_back(f); // rule - expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - break; - default: - args.push_back(f); - if(! f2.isNull()){ - args.push_back(f2); - } - expr = MK_EXPR(kind, args); + args.push_back(f); + if(! f2.isNull()){ + args.push_back(f2); } + expr = MK_EXPR(kind, args); } | LPAREN_TOK COMPREHENSION_TOK { PARSER_STATE->pushScope(true); } @@ -1902,33 +1848,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] } )+ RPAREN_TOK { - if(attr == ":rewrite-rule") { - Expr guard; - Expr body; - if(expr[1].getKind() == kind::IMPLIES || - expr[1].getKind() == kind::EQUAL) { - guard = expr[0]; - body = expr[1]; - } else { - guard = MK_CONST(bool(true)); - body = expr; - } - expr2 = guard; - args.push_back(body[0]); - args.push_back(body[1]); - if(!f2.isNull()) { - args.push_back(f2); - } - - if( body.getKind()==kind::IMPLIES ){ - kind = kind::RR_DEDUCTION; - }else if( body.getKind()==kind::EQUAL ){ - kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE; - }else{ - PARSER_STATE->parseError("Error parsing rewrite rule."); - } - expr = MK_EXPR( kind, args ); - } else if(! patexprs.empty()) { + if(! patexprs.empty()) { if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ for( size_t i=0; i<f2.getNumChildren(); i++ ){ if( f2[i].getKind()==kind::INST_PATTERN ){ @@ -2702,9 +2622,6 @@ GET_MODEL_TOK : 'get-model'; BLOCK_MODEL_TOK : 'block-model'; BLOCK_MODEL_VALUES_TOK : 'block-model-values'; ECHO_TOK : 'echo'; -REWRITE_RULE_TOK : 'assert-rewrite'; -REDUCTION_RULE_TOK : 'assert-reduction'; -PROPAGATION_RULE_TOK : 'assert-propagation'; DECLARE_SORTS_TOK : 'declare-sorts'; DECLARE_FUNS_TOK : 'declare-funs'; DECLARE_PREDS_TOK : 'declare-preds'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3ab3c0eb1..9800cbe91 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -626,33 +626,6 @@ void Smt2::resetAssertions() { } } -std::unique_ptr<Command> Smt2::assertRewriteRule( - Kind kind, - Expr bvl, - const std::vector<Expr>& triggers, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body) -{ - assert(kind == kind::RR_REWRITE || kind == kind::RR_REDUCTION - || kind == kind::RR_DEDUCTION); - - ExprManager* em = getExprManager(); - - std::vector<Expr> args; - args.push_back(mkAnd(heads)); - args.push_back(body); - - if (!triggers.empty()) - { - args.push_back(em->mkExpr(kind::INST_PATTERN_LIST, triggers)); - } - - Expr rhs = em->mkExpr(kind, args); - Expr rule = em->mkExpr(kind::REWRITE_RULE, bvl, mkAnd(guards), rhs); - return std::unique_ptr<Command>(new AssertCommand(rule, false)); -} - Smt2::SynthFunFactory::SynthFunFactory( Smt2* smt2, const std::string& fun, diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 6c1275115..6427b32d5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -198,24 +198,6 @@ class Smt2 : public Parser void resetAssertions(); /** - * Creates a command that asserts a rule. - * - * @param kind The kind of rule (RR_REWRITE, RR_REDUCTION, RR_DEDUCTION) - * @param bvl Bound variable list - * @param triggers List of triggers - * @param guards List of guards - * @param heads List of heads - * @param body The body of the rule - * @return The command that asserts the rewrite rule - */ - std::unique_ptr<Command> assertRewriteRule(Kind kind, - Expr bvl, - const std::vector<Expr>& triggers, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body); - - /** * Class for creating instances of `SynthFunCommand`s. Creating an instance * of this class pushes the scope, destroying it pops the scope. */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 17d8cbed5..ce8d4fa88 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2841,251 +2841,4 @@ std::string DatatypeDeclarationCommand::getCommandName() const return "declare-datatypes"; } -/* -------------------------------------------------------------------------- */ -/* class RewriteRuleCommand */ -/* -------------------------------------------------------------------------- */ - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - Expr head, - Expr body, - const Triggers& triggers) - : d_vars(vars), - d_guards(guards), - d_head(head), - d_body(body), - d_triggers(triggers) -{ -} - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - Expr head, - Expr body) - : d_vars(vars), d_head(head), d_body(body) -{ -} - -const std::vector<Expr>& RewriteRuleCommand::getVars() const { return d_vars; } -const std::vector<Expr>& RewriteRuleCommand::getGuards() const -{ - return d_guards; -} - -Expr RewriteRuleCommand::getHead() const { return d_head; } -Expr RewriteRuleCommand::getBody() const { return d_body; } -const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const -{ - return d_triggers; -} - -void RewriteRuleCommand::invoke(SmtEngine* smtEngine) -{ - try - { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if (d_guards.size() == 0) - guards = em->mkConst<bool>(true); - else if (d_guards.size() == 1) - guards = d_guards[0]; - else - guards = em->mkExpr(kind::AND, d_guards); - /** build expression */ - Expr expr; - if (d_triggers.empty()) - { - expr = em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body); - } - else - { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for (Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); - i != end; - ++i) - { - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers); - expr = - em->mkExpr(kind::RR_REWRITE, vars, guards, d_head, d_body, triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - /** Convert variables */ - VExpr vars = ExportTo(exprManager, variableMap, d_vars); - /** Convert guards */ - VExpr guards = ExportTo(exprManager, variableMap, d_guards); - /** Convert triggers */ - Triggers triggers; - triggers.reserve(d_triggers.size()); - for (const std::vector<Expr>& trigger_list : d_triggers) - { - triggers.push_back(ExportTo(exprManager, variableMap, trigger_list)); - } - /** Convert head and body */ - Expr head = d_head.exportTo(exprManager, variableMap); - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new RewriteRuleCommand(vars, guards, head, body, triggers); -} - -Command* RewriteRuleCommand::clone() const -{ - return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); -} - -std::string RewriteRuleCommand::getCommandName() const -{ - return "rewrite-rule"; -} - -/* -------------------------------------------------------------------------- */ -/* class PropagateRuleCommand */ -/* -------------------------------------------------------------------------- */ - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body, - const Triggers& triggers, - bool deduction) - : d_vars(vars), - d_guards(guards), - d_heads(heads), - d_body(body), - d_triggers(triggers), - d_deduction(deduction) -{ -} - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& heads, - Expr body, - bool deduction) - : d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) -{ -} - -const std::vector<Expr>& PropagateRuleCommand::getVars() const -{ - return d_vars; -} - -const std::vector<Expr>& PropagateRuleCommand::getGuards() const -{ - return d_guards; -} - -const std::vector<Expr>& PropagateRuleCommand::getHeads() const -{ - return d_heads; -} - -Expr PropagateRuleCommand::getBody() const { return d_body; } -const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const -{ - return d_triggers; -} - -bool PropagateRuleCommand::isDeduction() const { return d_deduction; } -void PropagateRuleCommand::invoke(SmtEngine* smtEngine) -{ - try - { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if (d_guards.size() == 0) - guards = em->mkConst<bool>(true); - else if (d_guards.size() == 1) - guards = d_guards[0]; - else - guards = em->mkExpr(kind::AND, d_guards); - /** build heads list */ - Expr heads; - if (d_heads.size() == 1) - heads = d_heads[0]; - else - heads = em->mkExpr(kind::AND, d_heads); - /** build expression */ - Expr expr; - if (d_triggers.empty()) - { - expr = em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body); - } - else - { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for (Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); - i != end; - ++i) - { - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN, *i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST, vtriggers); - expr = - em->mkExpr(kind::RR_REWRITE, vars, guards, heads, d_body, triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) -{ - /** Convert variables */ - VExpr vars = ExportTo(exprManager, variableMap, d_vars); - /** Convert guards */ - VExpr guards = ExportTo(exprManager, variableMap, d_guards); - /** Convert heads */ - VExpr heads = ExportTo(exprManager, variableMap, d_heads); - /** Convert triggers */ - Triggers triggers; - triggers.reserve(d_triggers.size()); - for (const std::vector<Expr>& trigger_list : d_triggers) - { - triggers.push_back(ExportTo(exprManager, variableMap, trigger_list)); - } - /** Convert head and body */ - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new PropagateRuleCommand(vars, guards, heads, body, triggers); -} - -Command* PropagateRuleCommand::clone() const -{ - return new PropagateRuleCommand( - d_vars, d_guards, d_heads, d_body, d_triggers); -} - -std::string PropagateRuleCommand::getCommandName() const -{ - return "propagate-rule"; -} } // namespace CVC4 diff --git a/src/smt/command.h b/src/smt/command.h index d82399135..19b858bd6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1315,80 +1315,6 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command std::string getCommandName() const override; }; /* class DatatypeDeclarationCommand */ -class CVC4_PUBLIC RewriteRuleCommand : public Command -{ - public: - typedef std::vector<std::vector<Expr> > Triggers; - - protected: - typedef std::vector<Expr> VExpr; - VExpr d_vars; - VExpr d_guards; - Expr d_head; - Expr d_body; - Triggers d_triggers; - - public: - RewriteRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - Expr head, - Expr body, - const Triggers& d_triggers); - RewriteRuleCommand(const std::vector<Expr>& vars, Expr head, Expr body); - - const std::vector<Expr>& getVars() const; - const std::vector<Expr>& getGuards() const; - Expr getHead() const; - Expr getBody() const; - const Triggers& getTriggers() const; - - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - Command* clone() const override; - std::string getCommandName() const override; -}; /* class RewriteRuleCommand */ - -class CVC4_PUBLIC PropagateRuleCommand : public Command -{ - public: - typedef std::vector<std::vector<Expr> > Triggers; - - protected: - typedef std::vector<Expr> VExpr; - VExpr d_vars; - VExpr d_guards; - VExpr d_heads; - Expr d_body; - Triggers d_triggers; - bool d_deduction; - - public: - PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body, - const Triggers& d_triggers, - /* true if we want a deduction rule */ - bool d_deduction = false); - PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& heads, - Expr body, - bool d_deduction = false); - - const std::vector<Expr>& getVars() const; - const std::vector<Expr>& getGuards() const; - const std::vector<Expr>& getHeads() const; - Expr getBody() const; - const Triggers& getTriggers() const; - bool isDeduction() const; - void invoke(SmtEngine* smtEngine) override; - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - Command* clone() const override; - std::string getCommandName() const override; -}; /* class PropagateRuleCommand */ - class CVC4_PUBLIC ResetCommand : public Command { public: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ad4d4e1d5..1d96fc207 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3630,12 +3630,6 @@ void SmtEnginePrivate::addFormula( // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); } - // rewrite rules are by default in the unsat core because - // they need to be applied until saturation - if(options::unsatCores() && - n.getKind() == kind::REWRITE_RULE ){ - ProofManager::currentPM()->addUnsatCore(n.toExpr()); - } ); // Add the normalized formula to the queue diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index dc11ed562..1534d2d4d 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -55,25 +55,4 @@ typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeType typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule -# for rewrite rules -# types... -sort RRHB_TYPE \ - Cardinality::INTEGERS \ - not-well-founded \ - "head and body of the rule type (for rewrite-rules theory)" - -# operators... - -# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE -operator REWRITE_RULE 3 "general rewrite rule (for rewrite-rules theory)" -#HEAD/BODY/TRIGGER -operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)" -operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)" -operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)" - -typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule -typerule RR_REWRITE ::CVC4::theory::quantifiers::RRRewriteTypeRule -typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule -typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule - endtheory diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 0e6eb1581..af4011bd9 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -16,7 +16,6 @@ #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -80,12 +79,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; QuantInstLevelAttribute qila; n.setAttribute( qila, lvl ); - }else if( attr=="rr-priority" ){ - Assert(node_values.size() == 1); - uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong(); - Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; - RrPriorityAttribute rrpa; - n.setAttribute( rrpa, lvl ); }else if( attr=="quant-elim" ){ Trace("quant-attr-debug") << "Set quantifier elimination " << n << std::endl; QuantElimAttribute qea; @@ -97,21 +90,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve } } -bool QuantAttributes::checkRewriteRule( Node q ) { - return !getRewriteRule( q ).isNull(); -} - -Node QuantAttributes::getRewriteRule( Node q ) { - if (q.getKind() == FORALL && q.getNumChildren() == 3 - && q[2][0].getNumChildren() > 0 - && q[2][0][0].getKind() == REWRITE_RULE) - { - return q[2][0][0]; - }else{ - return Node::null(); - } -} - bool QuantAttributes::checkFunDef( Node q ) { return !getFunDefHead( q ).isNull(); } @@ -275,10 +253,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl; } - if( avar.hasAttribute(RrPriorityAttribute()) ){ - qa.d_rr_priority = avar.getAttribute(RrPriorityAttribute()); - Trace("quant-attr") << "Attribute : rr priority " << qa.d_rr_priority << " : " << q << std::endl; - } if( avar.getAttribute(QuantElimAttribute()) ){ Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl; qa.d_quant_elim = true; @@ -294,11 +268,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_qid_num = avar; Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl; } - if( avar.getKind()==REWRITE_RULE ){ - Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; - Assert(i == 0); - qa.d_rr = avar; - } } } } @@ -349,15 +318,6 @@ int QuantAttributes::getQuantInstLevel( Node q ) { } } -int QuantAttributes::getRewriteRulePriority( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return -1; - }else{ - return it->second.d_rr_priority; - } -} - bool QuantAttributes::isQuantElim( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it==d_qattr.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 827c5e7f4..fc0f85956 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -111,7 +111,6 @@ struct QAttributes d_conjecture(false), d_axiom(false), d_sygus(false), - d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false) @@ -120,9 +119,6 @@ struct QAttributes ~QAttributes(){} /** does the quantified formula have a pattern? */ bool d_hasPattern; - /** if non-null, this is the rewrite rule representation of the quantified - * formula */ - Node d_rr; /** is this formula marked a conjecture? */ bool d_conjecture; /** is this formula marked an axiom? */ @@ -134,8 +130,6 @@ struct QAttributes bool d_sygus; /** side condition for sygus conjectures */ Node d_sygusSideCondition; - /** if a rewrite rule, then this is the priority value for the rewrite rule */ - int d_rr_priority; /** stores the maximum instantiation level allowed for this quantified formula * (-1 means allow any) */ int d_qinstLevel; @@ -150,8 +144,6 @@ struct QAttributes Node d_name; /** the quantifier id associated with this formula */ Node d_qid_num; - /** is this quantified formula a rewrite rule? */ - bool isRewriteRule() const { return !d_rr.isNull(); } /** is this quantified formula a function definition? */ bool isFunDef() const { return !d_fundef_f.isNull(); } /** @@ -193,10 +185,6 @@ public: /** compute the attributes for q */ void computeAttributes(Node q); - /** is quantifier treated as a rewrite rule? */ - static bool checkRewriteRule( Node q ); - /** get the rewrite rule associated with the quanfied formula */ - static Node getRewriteRule( Node q ); /** is fun def */ static bool checkFunDef( Node q ); /** is fun def */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e35595287..e2ee99ceb 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,15 +185,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { //compute attributes QAttributes qa; QuantAttributes::computeQuantAttributes( in, qa ); - if( !qa.isRewriteRule() ){ - for( int op=0; op<COMPUTE_LAST; op++ ){ - if( doOperation( in, op, qa ) ){ - ret = computeOperation( in, op, qa ); - if( ret!=in ){ - rew_op = op; - status = REWRITE_AGAIN_FULL; - break; - } + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, op, qa ) ){ + ret = computeOperation( in, op, qa ); + if( ret!=in ){ + rew_op = op; + status = REWRITE_AGAIN_FULL; + break; } } } @@ -2088,102 +2086,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut } } - -Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { - Kind rrkind = r[2].getKind(); - - //guards, pattern, body - - // Replace variables by Inst_* variable and tag the terms that contain them - std::vector<Node> vars; - vars.reserve(r[0].getNumChildren()); - for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){ - vars.push_back(*v); - }; - - // Body/Remove_term/Guards/Triggers - Node body = r[2][1]; - TNode new_terms = r[2][1]; - std::vector<Node> guards; - std::vector<Node> pattern; - Node true_node = NodeManager::currentNM()->mkConst(true); - // shortcut - TNode head = r[2][0]; - switch(rrkind){ - case kind::RR_REWRITE: - // Equality - pattern.push_back( head ); - body = head.eqNode(body); - break; - case kind::RR_REDUCTION: - case kind::RR_DEDUCTION: - // Add head to guards and pattern - switch(head.getKind()){ - case kind::AND: - for( unsigned i = 0; i<head.getNumChildren(); i++ ){ - guards.push_back(head[i]); - pattern.push_back(head[i]); - } - break; - default: - if( head!=true_node ){ - guards.push_back(head); - pattern.push_back( head ); - } - break; - } - break; - default: Unreachable() << "RewriteRules can be of only three kinds"; break; - } - // Add the other guards - TNode g = r[1]; - switch(g.getKind()){ - case kind::AND: - for( unsigned i = 0; i<g.getNumChildren(); i++ ){ - guards.push_back(g[i]); - } - break; - default: - if( g != true_node ){ - guards.push_back( g ); - } - break; - } - // Add the other triggers - if( r[2].getNumChildren() >= 3 ){ - for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) { - pattern.push_back( r[2][2][0][i] ); - } - } - - Trace("rr-rewrite") << "Rule is " << r << std::endl; - Trace("rr-rewrite") << "Head is " << head << std::endl; - Trace("rr-rewrite") << "Patterns are "; - for( unsigned i=0; i<pattern.size(); i++ ){ - Trace("rr-rewrite") << pattern[i] << " "; - } - Trace("rr-rewrite") << std::endl; - - NodeBuilder<> forallB(kind::FORALL); - forallB << r[0]; - Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) ); - gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body ); - gg = Rewriter::rewrite( gg ); - forallB << gg; - NodeBuilder<> patternB(kind::INST_PATTERN); - patternB.append(pattern); - NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); - //the entire rewrite rule is the first pattern - if( options::quantRewriteRules() ){ - patternListB << NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, r ); - } - patternListB << static_cast<Node>(patternB); - forallB << static_cast<Node>(patternListB); - Node rn = (Node) forallB; - - return rn; -} - bool QuantifiersRewriter::isPrenexNormalForm( Node n ) { if( n.getKind()==FORALL ){ return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] ); @@ -2272,17 +2174,14 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { Node prev = n; - if( n.getKind() == kind::REWRITE_RULE ){ - n = quantifiers::QuantifiersRewriter::rewriteRewriteRule( n ); - }else{ - if( options::preSkolemQuant() ){ - if( !isInst || !options::preSkolemQuantNested() ){ - Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; - //apply pre-skolemization to existential quantifiers - std::vector< TypeNode > fvTypes; - std::vector< TNode > fvs; - n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); - } + + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + //apply pre-skolemization to existential quantifiers + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs ); } } //pull all quantifiers globally @@ -2291,7 +2190,7 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { { Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; std::map< unsigned, std::map< Node, Node > > visited; - n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited ); + n = computePrenexAgg( n, true, visited ); n = Rewriter::rewrite( n ); Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; //Assert( isPrenexNormalForm( n ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e8f069882..69e057c76 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -204,7 +204,6 @@ private: private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: - static Node rewriteRewriteRule( Node r ); static bool isPrenexNormalForm( Node n ); /** preprocess * diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp deleted file mode 100644 index 9903456c9..000000000 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ /dev/null @@ -1,309 +0,0 @@ -/********************* */ -/*! \file rewrite_engine.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 Rewrite engine module - ** - ** This class manages rewrite rules for quantifiers - **/ - -#include "theory/quantifiers/rewrite_engine.h" - -#include "options/quantifiers_options.h" -#include "theory/quantifiers_engine.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - -struct PrioritySort { - std::vector< double > d_priority; - bool operator() (int i,int j) { - return d_priority[i] < d_priority[j]; - } -}; - -RewriteEngine::RewriteEngine(context::Context* c, - QuantifiersEngine* qe, - QuantConflictFind* qcf) - : QuantifiersModule(qe), d_qcf(qcf) -{ - d_needsSort = false; -} - -double RewriteEngine::getPriority( Node f ) { - Node rr = QuantAttributes::getRewriteRule( f ); - Node rrr = rr[2]; - Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; - bool deterministic = rrr[1].getKind()!=OR; - - if( rrr.getKind()==RR_REWRITE ){ - return deterministic ? 0.0 : 3.0; - }else if( rrr.getKind()==RR_DEDUCTION ){ - return deterministic ? 1.0 : 4.0; - }else if( rrr.getKind()==RR_REDUCTION ){ - return deterministic ? 2.0 : 5.0; - }else{ - return 6.0; - } - - //return deterministic ? 0.0 : 1.0; -} - -bool RewriteEngine::needsCheck( Theory::Effort e ){ - return e==Theory::EFFORT_FULL; - //return e>=Theory::EFFORT_LAST_CALL; -} - -void RewriteEngine::check(Theory::Effort e, QEffort quant_e) -{ - if (quant_e == QEFFORT_STANDARD) - { - Assert(!d_quantEngine->inConflict()); - Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; - //if( e==Theory::EFFORT_LAST_CALL ){ - // if( !d_quantEngine->getModel()->isModelSet() ){ - // d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); - // } - //} - if( d_needsSort ){ - d_priority_order.clear(); - PrioritySort ps; - std::vector< int > indicies; - for( int i=0; i<(int)d_rr_quant.size(); i++ ){ - ps.d_priority.push_back( getPriority( d_rr_quant[i] ) ); - indicies.push_back( i ); - } - std::sort( indicies.begin(), indicies.end(), ps ); - for( unsigned i=0; i<indicies.size(); i++ ){ - d_priority_order.push_back( d_rr_quant[indicies[i]] ); - } - d_needsSort = false; - } - - //apply rewrite rules - int addedLemmas = 0; - //per priority level - int index = 0; - bool success = true; - while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) { - addedLemmas += checkRewriteRule( d_priority_order[index], e ); - index++; - if( index<(int)d_priority_order.size() ){ - success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] ); - } - } - - Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl; - } -} - -int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { - Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl; - - // get the proper quantifiers info - std::map<Node, QuantInfo>::iterator it = d_qinfo.find(f); - if (it == d_qinfo.end()) - { - Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl; - return 0; - } - // reset QCF module - QuantInfo* qi = &it->second; - if (!qi->matchGeneratorIsValid()) - { - Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl; - return 0; - } - d_qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT); - Node rr = QuantAttributes::getRewriteRule(f); - Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; - qi->reset_round(d_qcf); - Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; - int addedLemmas = 0; - while (!d_quantEngine->inConflict() && qi->getNextMatch(d_qcf) - && (addedLemmas == 0 || !options::rrOneInstPerRound())) - { - Trace("rewrite-engine-inst-debug") - << " Got match to complete..." << std::endl; - qi->debugPrintMatch("rewrite-engine-inst-debug"); - std::vector<int> assigned; - if (!qi->isMatchSpurious(d_qcf)) - { - bool doContinue = false; - bool success = true; - int tempAddedLemmas = 0; - while (!d_quantEngine->inConflict() && tempAddedLemmas == 0 && success - && (addedLemmas == 0 || !options::rrOneInstPerRound())) - { - success = qi->completeMatch(d_qcf, assigned, doContinue); - doContinue = true; - if (success) - { - Trace("rewrite-engine-inst-debug") - << " Construct match..." << std::endl; - std::vector<Node> inst; - qi->getMatch(inst); - if (Trace.isOn("rewrite-engine-inst-debug")) - { - Trace("rewrite-engine-inst-debug") - << " Add instantiation..." << std::endl; - for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; - i++) - { - Trace("rewrite-engine-inst-debug") << " " << f[0][i] << " -> "; - if (i < inst.size()) - { - Trace("rewrite-engine-inst-debug") << inst[i] << std::endl; - } - else - { - Trace("rewrite-engine-inst-debug") - << "OUT_OF_RANGE" << std::endl; - Assert(false); - } - } - } - // resize to remove auxiliary variables - if (inst.size() > f[0].getNumChildren()) - { - inst.resize(f[0].getNumChildren()); - } - if (d_quantEngine->getInstantiate()->addInstantiation(f, inst)) - { - addedLemmas++; - tempAddedLemmas++; - } - else - { - Trace("rewrite-engine-inst-debug") << " - failed." << std::endl; - } - Trace("rewrite-engine-inst-debug") - << " Get next completion..." << std::endl; - } - } - Trace("rewrite-engine-inst-debug") - << " - failed to complete." << std::endl; - } - else - { - Trace("rewrite-engine-inst-debug") - << " - match is spurious." << std::endl; - } - Trace("rewrite-engine-inst-debug") << " Get next match..." << std::endl; - } - d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas; - Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl; - return addedLemmas; -} - -void RewriteEngine::registerQuantifier( Node f ) { - Node rr = QuantAttributes::getRewriteRule( f ); - if (rr.isNull()) - { - return; - } - Trace("rr-register") << "Register quantifier " << f << std::endl; - Trace("rr-register") << " rewrite rule is : " << rr << std::endl; - d_rr_quant.push_back(f); - d_rr[f] = rr; - d_needsSort = true; - Trace("rr-register") << " guard is : " << d_rr[f][1] << std::endl; - - std::vector<Node> qcfn_c; - - std::vector<Node> bvl; - bvl.insert(bvl.end(), f[0].begin(), f[0].end()); - - NodeManager* nm = NodeManager::currentNM(); - std::vector<Node> cc; - // add patterns - for (unsigned i = 1, nchild = f[2].getNumChildren(); i < nchild; i++) - { - std::vector<Node> nc; - for (const Node& pat : f[2][i]) - { - Node nn; - Node nbv = nm->mkBoundVar(pat.getType()); - if (pat.getType().isBoolean() && pat.getKind() != APPLY_UF) - { - nn = pat.negate(); - } - else - { - nn = pat.eqNode(nbv).negate(); - bvl.push_back(nbv); - } - nc.push_back(nn); - } - if (!nc.empty()) - { - Node n = nc.size() == 1 ? nc[0] : nm->mkNode(AND, nc); - Trace("rr-register-debug") << " pattern is " << n << std::endl; - if (std::find(cc.begin(), cc.end(), n) == cc.end()) - { - cc.push_back(n); - } - } - } - qcfn_c.push_back(nm->mkNode(BOUND_VAR_LIST, bvl)); - - std::vector<Node> body_c; - // add the guards - if (d_rr[f][1].getKind() == AND) - { - for (const Node& g : d_rr[f][1]) - { - if (MatchGen::isHandled(g)) - { - body_c.push_back(g.negate()); - } - } - } - else if (d_rr[f][1] != d_quantEngine->getTermUtil()->d_true) - { - if (MatchGen::isHandled(d_rr[f][1])) - { - body_c.push_back(d_rr[f][1].negate()); - } - } - // add the patterns to the body - body_c.push_back(cc.size() == 1 ? cc[0] : nm->mkNode(AND, cc)); - // make the body - qcfn_c.push_back(body_c.size() == 1 ? body_c[0] : nm->mkNode(OR, body_c)); - // make the quantified formula - d_qinfo_n[f] = nm->mkNode(FORALL, qcfn_c); - Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl; - d_qinfo[f].initialize(d_qcf, d_qinfo_n[f], d_qinfo_n[f][1]); -} - -void RewriteEngine::assertNode( Node n ) { - -} - -bool RewriteEngine::checkCompleteFor( Node q ) { - // by semantics of rewrite rules, saturation -> SAT - return std::find( d_rr_quant.begin(), d_rr_quant.end(), q )!=d_rr_quant.end(); -} - -Node RewriteEngine::getInstConstNode( Node n, Node q ) { - std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); - if( it==d_inst_const_node[q].end() ){ - Node nn = - d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants( - n, q); - d_inst_const_node[q][n] = nn; - return nn; - }else{ - return it->second; - } -} diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h deleted file mode 100644 index 29aba0f1a..000000000 --- a/src/theory/quantifiers/rewrite_engine.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file rewrite_engine.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 - ** - ** [[ Add lengthier description here ]] - ** \todo document this file -**/ - -#include "cvc4_private.h" - -#ifndef CVC4__REWRITE_ENGINE_H -#define CVC4__REWRITE_ENGINE_H - -#include <map> -#include <vector> - -#include "expr/attribute.h" -#include "theory/quantifiers/ematching/trigger.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers/quant_util.h" - -namespace CVC4 { -namespace theory { - -/** - * An attribute for marking a priority value for rewrite rules. - */ -struct RrPriorityAttributeId -{ -}; -typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute; - -namespace quantifiers { - -class RewriteEngine : public QuantifiersModule -{ - std::vector< Node > d_rr_quant; - std::vector< Node > d_priority_order; - std::map< Node, Node > d_rr; - /** explicitly provided patterns */ - std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; - /** get the quantifer info object */ - std::map< Node, Node > d_qinfo_n; - std::map< Node, QuantInfo > d_qinfo; - double getPriority( Node f ); - bool d_needsSort; - std::map< Node, std::map< Node, Node > > d_inst_const_node; - Node getInstConstNode( Node n, Node q ); - - private: - int checkRewriteRule( Node f, Theory::Effort e ); - - public: - RewriteEngine(context::Context* c, - QuantifiersEngine* qe, - QuantConflictFind* qcf); - - bool needsCheck(Theory::Effort e) override; - void check(Theory::Effort e, QEffort quant_e) override; - void registerQuantifier(Node f) override; - void assertNode(Node n) override; - bool checkCompleteFor(Node q) override; - /** Identify this module */ - std::string identify() const override { return "RewriteEngine"; } - - private: - /** - * A pointer to the quantifiers conflict find module of the quantifiers - * engine. This is the module that computes instantiations for rewrite rule - * quantifiers. - */ - QuantConflictFind* d_qcf; -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index a83dbf541..e2c9043a1 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -141,91 +141,6 @@ struct QuantifierInstClosureTypeRule { } };/* struct QuantifierInstClosureTypeRule */ - -class RewriteRuleTypeRule { -public: - - /** - * Compute the type for (and optionally typecheck) a term belonging - * to the theory of rewriterules. - * - * @param nodeManager the NodeManager in use - * @param n the node to compute the type of - * @param check if true, the node's type should be checked as well - * as computed. - */ - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) - { - Debug("typecheck-r") << "type check for rr " << n << std::endl; - Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren() == 3); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate(n[0], - "first argument of rewrite rule is not bound var list"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n[1], - "guard of rewrite rule is not an actual guard"); - } - if( n[2].getType(check) != - TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){ - throw TypeCheckingExceptionPrivate(n[2], - "not a correct rewrite rule"); - } - } - return nodeManager->booleanType(); - } -};/* class RewriteRuleTypeRule */ - -class RRRewriteTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::RR_REWRITE); - if( check ){ - if( n[0].getType(check)!=n[1].getType(check) ){ - throw TypeCheckingExceptionPrivate(n, - "terms of rewrite rule are not equal"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n[0].getKind()!=kind::APPLY_UF ){ - throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation"); - } - } - return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - -class RRRedDedTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - Assert(n.getKind() == kind::RR_REDUCTION - || n.getKind() == kind::RR_DEDUCTION); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){ - throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); - } - } - return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c7eafc3b8..80a493496 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,6 @@ #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/sygus/synth_engine.h" #include "theory/sep/theory_sep.h" #include "theory/theory_engine.h" @@ -53,7 +52,6 @@ class QuantifiersEnginePrivate d_model_engine(nullptr), d_bint(nullptr), d_qcf(nullptr), - d_rr_engine(nullptr), d_sg_gen(nullptr), d_synth_e(nullptr), d_lte_part_inst(nullptr), @@ -81,8 +79,6 @@ class QuantifiersEnginePrivate std::unique_ptr<quantifiers::BoundedIntegers> d_bint; /** Conflict find mechanism for quantifiers */ std::unique_ptr<quantifiers::QuantConflictFind> d_qcf; - /** rewrite rules utility */ - std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine; /** subgoal generator */ std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen; /** ceg instantiation */ @@ -111,7 +107,7 @@ class QuantifiersEnginePrivate bool& needsBuilder) { // add quantifiers modules - if (options::quantConflictFind() || options::quantRewriteRules()) + if (options::quantConflictFind()) { d_qcf.reset(new quantifiers::QuantConflictFind(qe, c)); modules.push_back(d_qcf.get()); @@ -150,11 +146,6 @@ class QuantifiersEnginePrivate // finite model finder has special ways of building the model needsBuilder = true; } - if (options::quantRewriteRules()) - { - d_rr_engine.reset(new quantifiers::RewriteEngine(c, qe, d_qcf.get())); - modules.push_back(d_rr_engine.get()); - } if (options::ltePartialInst()) { d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c)); @@ -397,16 +388,6 @@ void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa) { - if (!qa.d_rr.isNull()) - { - if (d_private->d_rr_engine.get() == nullptr) - { - Trace("quant-warn") << "WARNING : rewrite engine is null, and we have : " - << q << std::endl; - } - // set rewrite engine as owner - setOwner(q, d_private->d_rr_engine.get(), 2); - } if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull())) { if (d_private->d_synth_e.get() == nullptr) diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 3b11d8e54..6a404104f 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -35,7 +35,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE + if ((parent.isClosure() || parent.getKind() == kind::SEP_STAR || parent.getKind() == kind::SEP_WAND || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) @@ -178,7 +178,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE + if ((parent.isClosure() || parent.getKind() == kind::SEP_STAR || parent.getKind() == kind::SEP_WAND || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) |