Age | Commit message (Collapse) | Author |
|
QuantConflictFind.
|
|
changes default behavior.
|
|
|
|
forms are dependent upon which equalities. Add anti-skolemization module to quantifiers. Disable rewriting of non-clashing equalities between same constructors.
|
|
fixes in quantifiers related to subtypes/parametric sorts. Make macros trace dependencies for get-unsat-core. Add regressions.
|
|
incomplete for fmc.
|
|
enumerator and codatatype rewriter, further simplify fmc.
|
|
|
|
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
|
|
|
|
|
|
restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
|
|
|
|
|
|
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
|
|
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
|
|
liberal.
|
|
|
|
symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
|
|
Enable redundant ITE branch elimination in quantifiers rewriter.
|
|
|
|
for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
|
|
soundness bug in strings related to explaining length terms.
|
|
(mostly whitespace differences).
|
|
|
|
|
|
|
|
instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs.
|
|
|
|
|
|
|
|
Add regressions.
|
|
minor changes.
|
|
This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
|
|
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
|
|
|
|
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
|
|
Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
|
|
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
|
|
success, nonzero error
|
|
|
|
|
|
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
|
|
|
|
Thanks to Peter Collingbourne for the report, and the patch!
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
|
|
should work now
|
|
problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381.
* Added LAMBDA kind and type rule, and Node::isClosure().
(this commit was certified error- and warning-free by the test-and-commit script.)
|