Age | Commit message (Collapse) | Author |
|
cases of nonterminating rewrite-rules regressions.
|
|
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.
|
|
bodies; fix bug 551, improper ITE removal under quantifiers.
|
|
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
|
|
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|
|
|
|
pattern first
just after the bindings
Do it before the release in order to not break user files later
|
|
|
|
417. oops. also fix spelling on "rewritting" test
|
|
should work now
|
|
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
|
|
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
|