Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
Improve datatypes rewrite, make option for previous dt semantics.
|
|
incorrectly applied selector terms.
|
|
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.
|
|
|
|
|
|
|
|
Fix for ite of >=64bit wide bitvectors with unconstrained condition.
|
|
Deligiannis and Jeroen Ketema for discovering this issue.
|
|
|
|
|
|
|
|
Sets model
|
|
|
|
Observed behavior:
--check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.
Issue:
The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)
Resolution:
adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().
|
|
(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)
|
|
|
|
|
|
|
|
|
|
|
|
signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
|
|
cases of nonterminating rewrite-rules regressions.
|
|
* Reenable parts of bvsimple test
* Fix typo in #endif comment
|
|
|
|
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.
|
|
|
|
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
|
|
|
|
This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
|
|
|
|
|
|
membership constraints
|
|
|
|
|
|
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.
|
|
|