summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/api/cvc4cppkind.h8
-rw-r--r--src/bindings/java/CMakeLists.txt2
-rw-r--r--src/options/quantifiers_options.toml9
-rw-r--r--src/parser/smt2/Smt2.g95
-rw-r--r--src/parser/smt2/smt2.cpp27
-rw-r--r--src/parser/smt2/smt2.h18
-rw-r--r--src/smt/command.cpp247
-rw-r--r--src/smt/command.h74
-rw-r--r--src/smt/smt_engine.cpp6
-rw-r--r--src/theory/quantifiers/kinds21
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp40
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h12
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp133
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h1
-rw-r--r--src/theory/quantifiers/rewrite_engine.cpp309
-rw-r--r--src/theory/quantifiers/rewrite_engine.h86
-rw-r--r--src/theory/quantifiers/theory_quantifiers_type_rules.h85
-rw-r--r--src/theory/quantifiers_engine.cpp21
-rw-r--r--src/theory/term_registration_visitor.cpp4
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())
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback