diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-20 09:45:46 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-11 11:29:45 -0500 |
| commit | 38d149261763e5f2f65abb21c2b647f2befa7807 (patch) | |
| tree | 51c3019eff61c7f3702f3dc888fb88d3a714f68a /src/theory/quantifiers/kinds | |
| parent | 3ed865aa12a94e935038d70b130701045b84a8b8 (diff) | |
Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.
Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.
QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master.
Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.
Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE.
Merging rewrite rules into master, check-model current fails on 3 FMF regressions.
Fix check-model issue, a line of code was omitted during merge.
Diffstat (limited to 'src/theory/quantifiers/kinds')
| -rw-r--r-- | src/theory/quantifiers/kinds | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index ab0e9d934..795bc1ab4 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -48,4 +48,25 @@ typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeR typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule +# for rewrite rules +# types... +sort RRHB_TYPE \ + Cardinality::INTEGERS \ + not-well-founded \ + "head and body of the rule type" + +# operators... + +# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE +operator REWRITE_RULE 3 "general rewrite rule" +#HEAD/BODY/TRIGGER +operator RR_REWRITE 2:3 "actual rewrite rule" +operator RR_REDUCTION 2:3 "actual reduction rule" +operator RR_DEDUCTION 2:3 "actual deduction rule" + +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 |