projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2014-10-13
ajreynol
CEGQI uses model. Enforce fairness in CEGQI natively.
commit
|
commitdiff
|
tree
2014-10-13
ajreynol
Model building into quantifiers engine. Simplify axiom...
commit
|
commitdiff
|
tree
2014-10-13
ajreynol
Refactor model builder from model engine to quant engin...
commit
|
commitdiff
|
tree
2014-10-11
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-11
Morgan Deters
Some defensive programming at destruction time, and...
commit
|
commitdiff
|
tree
2014-10-10
Kshitij Bansal
Merge remote-tracking branch 'origin/1.4.x'
commit
|
commitdiff
|
tree
2014-10-10
ajreynol
Initial draft of CEGQI.
commit
|
commitdiff
|
tree
2014-10-10
Kshitij Bansal
Fix issue with shared but non-preregistered term setup...
commit
|
commitdiff
|
tree
2014-10-10
Morgan Deters
Cleanup
commit
|
commitdiff
|
tree
2014-10-10
ajreynol
Add owner map to better manage QuantifiersModules....
commit
|
commitdiff
|
tree
2014-10-09
ajreynol
Refactor quantifier prenex option. By default, do...
commit
|
commitdiff
|
tree
2014-10-09
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-09
Morgan Deters
Add unsat cores support to CVC native language.
commit
|
commitdiff
|
tree
2014-10-08
Morgan Deters
Some minor cleanup.
commit
|
commitdiff
|
tree
2014-10-08
Morgan Deters
Remove private header from public driver.
commit
|
commitdiff
|
tree
2014-10-08
Kshitij Bansal
Fix portoflio issues (debugging code was being called...
commit
|
commitdiff
|
tree
2014-10-07
Kshitij Bansal
Merge remote-tracking branch 'upstream/master' into...
commit
|
commitdiff
|
tree
2014-10-07
Kshitij Bansal
update default Sets options
commit
|
commitdiff
|
tree
2014-10-07
Kshitij Bansal
whitespace fixes
commit
|
commitdiff
|
tree
2014-10-07
ajreynol
Cache for getInstance, thanks to Johannes Kanig for...
commit
|
commitdiff
|
tree
2014-10-07
Kshitij Bansal
add couple of stats
commit
|
commitdiff
|
tree
2014-10-07
Kshitij Bansal
sets stronger equality propagator
commit
|
commitdiff
|
tree
2014-10-07
ajreynol
Refactor quantifiers attributes.
commit
|
commitdiff
|
tree
2014-10-07
Morgan Deters
define-const is an extended command, not permitted...
commit
|
commitdiff
|
tree
2014-10-07
Morgan Deters
Fix unit test that was broken with last commit.
commit
|
commitdiff
|
tree
2014-10-07
Morgan Deters
Fix a resource limiting issue where interruption didn...
commit
|
commitdiff
|
tree
2014-10-07
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-07
Morgan Deters
Fix a bug in tuple-record handling. Thanks to Saumya...
commit
|
commitdiff
|
tree
2014-10-07
Morgan Deters
Some minor cleanup.
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Copyright-updating script now retains non-NYU/UIowa...
commit
|
commitdiff
|
tree
2014-10-06
Kshitij Bansal
fix for bug586
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Print array constants in SMT-LIB models with new syntax.
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Clear out decls/defs with RESET command.
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Extended parsing testcase, with constant arrays and...
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Fix native language parsing of chained-store expression...
commit
|
commitdiff
|
tree
2014-10-06
Morgan Deters
Support for RESET command in CVC native language (and...
commit
|
commitdiff
|
tree
2014-10-04
Morgan Deters
Enable some old bug testcases that (maybe?) never got...
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Support exporting array-store-all expressions to other...
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Fix output of integer-valued real constants in SMT...
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Add some (so far trivial) regressions for constant...
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Improve error in CVC parser in presence of unrecognized...
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
More array constants and parsing: better error messages...
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Minor fixes to CVC printer.
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
SMT-LIB parser support for array constants (Z3 syntax).
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Note array const support in NEWS
commit
|
commitdiff
|
tree
2014-10-03
Morgan Deters
Fix unit test for ArrayStoreAll.
commit
|
commitdiff
|
tree
2014-10-02
Clark Barrett
Added internal support for constant arrays.
commit
|
commitdiff
|
tree
2014-10-02
Morgan Deters
Merge branch '1.4.x'.
commit
|
commitdiff
|
tree
2014-10-02
Clark Barrett
Added option for developer use only
commit
|
commitdiff
|
tree
2014-10-02
Clark Barrett
More model-based combination for arrays
commit
|
commitdiff
|
tree
2014-10-02
Clark Barrett
Better getEqualityStatus for arrays, smarter combinatio...
commit
|
commitdiff
|
tree
2014-10-02
Morgan Deters
Update AUTHORS affiliations and add Martin.
commit
|
commitdiff
|
tree
2014-10-02
Morgan Deters
Fix comment in SmtEngine.
commit
|
commitdiff
|
tree
2014-10-02
Morgan Deters
Merge pull request #54 from kbansal/bugfix_setssegfault
commit
|
commitdiff
|
tree
2014-10-02
Kshitij Bansal
fix getModelValue(<non-preregistered term>)
commit
|
commitdiff
|
tree
2014-10-02
Morgan Deters
Fix for an array-of-record model generation assert...
commit
|
commitdiff
|
tree
2014-10-01
ajreynol
Option for more aggressive merging in UEE.
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Fix improper #inclusion of private header outside library.
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Fix a command-replay bug in tear-down-incremental mode...
commit
|
commitdiff
|
tree
2014-09-30
Morgan Deters
Proofs- and cores-related segfault fixes (mainly a...
commit
|
commitdiff
|
tree
2014-09-29
ajreynol
Add option for aggressive model filtering in conjecture...
commit
|
commitdiff
|
tree
2014-09-27
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-27
Morgan Deters
Fix infinite loop in --bitblast-aig/--bv-aig-simp options.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Fix bv options doc.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Fix some configuration-related oddness.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Clarify some licensing-related things.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Finer-grained resource-limiting in quantifiers.
commit
|
commitdiff
|
tree
2014-09-26
Morgan Deters
Fix AIG bitblaster for unsat cores.
commit
|
commitdiff
|
tree
2014-09-25
Morgan Deters
fix unit test for new fair datatype enumeration
commit
|
commitdiff
|
tree
2014-09-25
ajreynol
Fair datatype enumeration.
commit
|
commitdiff
|
tree
2014-09-24
ajreynol
Fix infinite loop in datatypes enumerator. Minor work...
commit
|
commitdiff
|
tree
2014-09-24
ajreynol
Refactor option for uf+cardinality constraints solver.
commit
|
commitdiff
|
tree
2014-09-24
ajreynol
Partial support for codatatype models.
commit
|
commitdiff
|
tree
2014-09-23
ajreynol
Support :no-pattern.
commit
|
commitdiff
|
tree
2014-09-23
ajreynol
Do not throw error when codatatype is not well-founded...
commit
|
commitdiff
|
tree
2014-09-18
Morgan Deters
Resource spending support in theories (and especially...
commit
|
commitdiff
|
tree
2014-09-18
Kshitij Bansal
cvc4terminate infinite loop fix
commit
|
commitdiff
|
tree
2014-09-18
Kshitij Bansal
cvc4terminate infinite loop fix
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Merge branch '1.4.x' while ignoring commit 8d5eb49.
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Fix fix. There are no unsat cores in 1.4
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Merge branch '1.4.x'
commit
|
commitdiff
|
tree
2014-09-17
Kshitij Bansal
Fix (push) and (pop). Thanks to Christoph Sticksel...
commit
|
commitdiff
|
tree
2014-09-17
ajreynol
Fix soundness bug for quantifier macros involving Int...
commit
|
commitdiff
|
tree
2014-09-17
ajreynol
Refactor entailment filtering for conjecture generator...
commit
|
commitdiff
|
tree
2014-09-17
ajreynol
More refactoring of conjecture generation. Term genera...
commit
|
commitdiff
|
tree
2014-09-16
ajreynol
Bug fix variable triggers with --inst-max-level : use...
commit
|
commitdiff
|
tree
2014-09-16
ajreynol
Refactoring of conjecture generator. Determine subgoal...
commit
|
commitdiff
|
tree
2014-09-09
ajreynol
Fix bug for variable term triggers within multi-triggers.
commit
|
commitdiff
|
tree
2014-09-08
ajreynol
Accept user-provided triggers with variable terms....
commit
|
commitdiff
|
tree
2014-09-04
Kshitij Bansal
Update command_executor_portfolio.cpp
commit
|
commitdiff
|
tree
2014-09-03
Kshitij Bansal
Merge remote-tracking branch 'origin/master'
commit
|
commitdiff
|
tree
2014-09-03
Kshitij Bansal
check() optimization
commit
|
commitdiff
|
tree
2014-09-03
ajreynol
Implement and enable --dt-var-exp-quant, cleanup trace...
commit
|
commitdiff
|
tree
2014-09-03
ajreynol
Work on conjecture generator : do not generalize subter...
commit
|
commitdiff
|
tree
next