projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false...
[cvc5.git]
/
src
/
theory
/
quantifiers_engine.cpp
2015-04-26
ajreynol
Bug fixes and improvements for mbqi with theory symbols...
blob
|
commitdiff
|
raw
2015-04-17
Kshitij Bansal
Merge pull request #72 from kbansal/decision-requirephase
blob
|
commitdiff
|
raw
|
diff to current
2015-04-09
ajreynol
Fix performance issue with variable triggers + instanti...
blob
|
commitdiff
|
raw
|
diff to current
2015-04-02
Kshitij Bansal
Merge pull request #71 from kbansal/const-are-triggers
blob
|
commitdiff
|
raw
|
diff to current
2015-04-01
ajreynol
Improvements and bug fixes related to cbqi/cegqi. ...
blob
|
commitdiff
|
raw
|
diff to current
2015-03-23
ajreynol
Decouple counter-example guided quantifier instantiatio...
blob
|
commitdiff
|
raw
|
diff to current
2015-03-11
ajreynol
Minor fixes and improvements to cegqi-si for linear...
blob
|
commitdiff
|
raw
|
diff to current
2015-02-06
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2015-02-04
ajreynol
Refactor sygus_util to TermDb. Initial work on solutio...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-29
ajreynol
Restrict LtePartialInst instantiations based on E-match...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-26
ajreynol
Output solutions for synthesis conjectures with --dump...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-24
ajreynol
Variable patterns only look at eligible terms. Minor...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-24
ajreynol
Add --lte-restrict-inst-closure option. Push dt.size...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-23
ajreynol
Rework inst-closure.
blob
|
commitdiff
|
raw
|
diff to current
2015-01-22
ajreynol
Add option --lte-partial-inst. Remove inst-closure.
blob
|
commitdiff
|
raw
|
diff to current
2014-12-03
Kshitij Bansal
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-11-28
ajreynol
Synchronize conjecture generation with E-matching....
blob
|
commitdiff
|
raw
|
diff to current
2014-11-27
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-11-25
ajreynol
Fix bug in --term-db-mode=relevant with variable trigge...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-20
ajreynol
Disable constants sharing in eq engine, disable hack...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-18
ajreynol
Compute model basis only for fmf. Add another co-datat...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-13
Morgan Deters
Merge pull request #69 from mdeters/bug594
blob
|
commitdiff
|
raw
|
diff to current
2014-11-13
ajreynol
Remove two obsolete versions of MBQI.
blob
|
commitdiff
|
raw
|
diff to current
2014-11-10
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
ajreynol
Enable --quant-cf by default. Fix bug in qcf for mixed...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
ajreynol
Properly distinguish which EQC to assign values in...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-05
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-17
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-16
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-13
ajreynol
CEGQI uses model. Enforce fairness in CEGQI natively.
blob
|
commitdiff
|
raw
|
diff to current
2014-10-13
ajreynol
Model building into quantifiers engine. Simplify axiom...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-13
ajreynol
Refactor model builder from model engine to quant engin...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-11
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-10
Kshitij Bansal
Merge remote-tracking branch 'origin/1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-10
ajreynol
Initial draft of CEGQI.
blob
|
commitdiff
|
raw
|
diff to current
2014-10-10
ajreynol
Add owner map to better manage QuantifiersModules....
blob
|
commitdiff
|
raw
|
diff to current
2014-10-09
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-07
Kshitij Bansal
Merge remote-tracking branch 'upstream/master' into...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-07
ajreynol
Cache for getInstance, thanks to Johannes Kanig for...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-07
ajreynol
Refactor quantifiers attributes.
blob
|
commitdiff
|
raw
|
diff to current
2014-10-07
Morgan Deters
Fix a resource limiting issue where interruption didn...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-07
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-06
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-06
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-03
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-03
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-02
Morgan Deters
Merge branch '1.4.x'.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-30
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-27
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-26
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-26
Morgan Deters
Finer-grained resource-limiting in quantifiers.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-24
ajreynol
Refactor option for uf+cardinality constraints solver.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-23
ajreynol
Do not throw error when codatatype is not well-founded...
blob
|
commitdiff
|
raw
|
diff to current
2014-09-18
Morgan Deters
Resource spending support in theories (and especially...
blob
|
commitdiff
|
raw
|
diff to current
2014-09-17
Kshitij Bansal
Merge branch '1.4.x' while ignoring commit 8d5eb49.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-17
Kshitij Bansal
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-16
ajreynol
Bug fix variable triggers with --inst-max-level : use...
blob
|
commitdiff
|
raw
|
diff to current
2014-09-08
ajreynol
Accept user-provided triggers with variable terms....
blob
|
commitdiff
|
raw
|
diff to current
2014-08-29
ajreynol
Set instantiation level on skolemized bodies of quantif...
blob
|
commitdiff
|
raw
|
diff to current
2014-08-26
ajreynol
Bug fixes for --purify-triggers, --dt-force-assignment.
blob
|
commitdiff
|
raw
|
diff to current
2014-08-25
ajreynol
New option --purify-triggers. Refactoring of InstMatch...
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-21
ajreynol
Avoid doing work in quantifiers engine when no quantifi...
blob
|
commitdiff
|
raw
|
diff to current
2014-08-20
ajreynol
Fix --inst-max-level for strategies that use arbitrary...
blob
|
commitdiff
|
raw
|
diff to current
2014-08-19
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-18
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-08-18
ajreynol
Add support for quantifier-specific instantiation level...
blob
|
commitdiff
|
raw
|
diff to current
2014-08-01
ajreynol
Minor cleanup from previous commit. Better organizatio...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-31
ajreynol
New module for generating candidate equality conjecture...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-10
Kshitij Bansal
Merge remote-tracking branch 'origin/master' into segfa...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-01
Morgan Deters
Update copyrights.
blob
|
commitdiff
|
raw
|
diff to current
2014-06-26
Morgan Deters
Merge tag 'smtcomp2014-resubmission'
blob
|
commitdiff
|
raw
|
diff to current
2014-06-22
Morgan Deters
Merge tag 'smtcomp2014-application'
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
ajreynol
More proof support for CASC : include skolemization
blob
|
commitdiff
|
raw
|
diff to current
2014-06-16
ajreynol
More proof support for CASC : include skolemization
blob
|
commitdiff
|
raw
|
diff to current
2014-05-30
ajreynol
Fixes for --inst-max-level
blob
|
commitdiff
|
raw
|
diff to current
2014-05-14
Andrew Reynolds
Finish --dump-instantiations option. Update scripts.
blob
|
commitdiff
|
raw
|
diff to current
2014-05-13
ajreynol
Add lazy strategy for bounded integers to avoid non...
blob
|
commitdiff
|
raw
|
diff to current
2014-05-13
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-05-12
Andrew Reynolds
Minor updates/fix to --cbqi-recurse
blob
|
commitdiff
|
raw
|
diff to current
2014-05-12
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-05-11
Andrew Reynolds
More preparation for CASC proofs. Minor fix for sort...
blob
|
commitdiff
|
raw
|
diff to current
2014-05-08
Andrew Reynolds
Fixes to quantifiers rewriter to prevent miniscoping...
blob
|
commitdiff
|
raw
|
diff to current
2014-05-06
Andrew Reynolds
First draft of ambqi_builder (new implementation of...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-30
Morgan Deters
Mostly resolves bug #561 memory leaks, and more.
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Kshitij Bansal
Merge pull request #25 from kbansal/sets
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Andrew Reynolds
Preparation for models for co-inductive datatypes....
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
ajreynol
Optimizations for datatypes: check for clashes modulo...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-28
Kshitij Bansal
Merge remote-tracking branch 'upstream/master' into...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-24
Andrew Reynolds
Add --inst-max-level=N option for Kshitij. Support...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-10
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-04-09
Kshitij Bansal
Merge pull request #24 from kbansal/sets-model
blob
|
commitdiff
|
raw
|
diff to current
2014-04-09
Andrew Reynolds
Handle fmf.card as input from user, add support in...
blob
|
commitdiff
|
raw
|
diff to current
2014-04-01
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-26
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
next