projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and string...
[cvc5.git]
/
src
/
smt
/
smt_engine.cpp
2015-04-09
ajreynol
Fix unsat-core issues related to rewrite rules, quantif...
blob
|
commitdiff
|
raw
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-16
Liana Hadarean
Fixed proof unitialized memory and minor memory leaks.
blob
|
commitdiff
|
raw
|
diff to current
2015-03-10
ajreynol
CNF proofs. Infrastructure for preprocessing proofs...
blob
|
commitdiff
|
raw
|
diff to current
2015-03-05
ajreynol
Minor fixes. Extend cegqi-si to real arithmetic.
blob
|
commitdiff
|
raw
|
diff to current
2015-03-04
ajreynol
More work on arithmetic single invocation synthesis...
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-02
ajreynol
Single invocation module for counterexample guided...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-27
ajreynol
Always miniscope nested quantifiers. Disable miniscopi...
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-22
ajreynol
Narrow sygus search space based on NNF and rewriting...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-22
ajreynol
Do not drop patterns during boolean term rewriting...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-13
Morgan Deters
Fix a memory issue in ResourceManager on 32-bit (resolv...
blob
|
commitdiff
|
raw
|
diff to current
2015-01-07
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-12-28
ajreynol
Disable prenex by default when using fmf bound int...
blob
|
commitdiff
|
raw
|
diff to current
2014-12-16
Morgan Deters
Fix oversight in dumping assertions in preprocessing.
blob
|
commitdiff
|
raw
|
diff to current
2014-12-04
Morgan Deters
Fix segfault in lambdas when constructed via API.
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-27
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-11-22
lianah
added number of resource units used as a stat
blob
|
commitdiff
|
raw
|
diff to current
2014-11-21
ajreynol
Change default option to --inst-when=full-last-call...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-19
Kshitij Bansal
Merge pull request #70 from kbansal/sets-for-merge...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-19
Kshitij Bansal
Set Constant's normal form and other short fixes
blob
|
commitdiff
|
raw
|
diff to current
2014-11-18
ajreynol
Add local theory extensions instantiation strategy...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-17
Liana Hadarean
Resource-limiting work.
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-11
Kshitij Bansal
Merge pull request #64 from mdeters/theorysets-hashset...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-10
Tianyi Liang
Merge pull request #63 from mdeters/theorystrings-hashs...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-10
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-11-09
Morgan Deters
Fix a deterministic assignment-ordering for get-assignm...
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
Morgan Deters
Corrected fix for missing case in model postprocessor...
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
Revert "Fix missing case in model postprocessor (resolv...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-07
Morgan Deters
Revert "Fix missing case in model postprocessor (resolv...
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
Fix missing case in model postprocessor (resolves bug...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-05
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-28
ajreynol
Preprocessing step for finding finite runs of well...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-23
Morgan Deters
Parsing and infrastructure support for SMT-LIBv2.5...
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
ajreynol
Make --user-pat=trust default. Fix a few warnings...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-16
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-14
Morgan Deters
Merge pull request #58 from mdeters/smt-attributes
blob
|
commitdiff
|
raw
|
diff to current
2014-10-14
Morgan Deters
Context-dependent expr attributes are now attached...
blob
|
commitdiff
|
raw
|
diff to current
2014-10-11
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-10-11
Morgan Deters
Some defensive programming at destruction time, and...
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-09
Morgan Deters
Merge branch '1.4.x'
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-06
Morgan Deters
Support for RESET command in CVC native language (and...
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-10-02
Morgan Deters
Fix comment in SmtEngine.
blob
|
commitdiff
|
raw
|
diff to current
2014-09-30
Morgan Deters
Merge branch '1.4.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-30
Morgan Deters
Proofs- and cores-related segfault fixes (mainly a...
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-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
Refactoring of conjecture generator. Determine subgoal...
blob
|
commitdiff
|
raw
|
diff to current
2014-09-03
Kshitij Bansal
Merge remote-tracking branch 'origin/master'
blob
|
commitdiff
|
raw
|
diff to current
2014-09-03
ajreynol
Implement and enable --dt-var-exp-quant, cleanup trace...
blob
|
commitdiff
|
raw
|
diff to current
2014-08-29
ajreynol
Do not use pure theory terms as single triggers. Minor...
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-23
Morgan Deters
Unsat core printing.
blob
|
commitdiff
|
raw
|
diff to current
2014-08-23
Morgan Deters
Some fixes for dump- and get-unsat-core.
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
One small thing forgotten in core commit.
blob
|
commitdiff
|
raw
|
diff to current
2014-08-22
Morgan Deters
Unsat core infrastruture and API (SMT-LIB compliance...
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-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-15
Kshitij Bansal
Update smt_engine.cpp
blob
|
commitdiff
|
raw
|
diff to current
2014-07-13
Morgan Deters
Fix a bug in Boolean terms and arrays. Thanks to Jean...
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-07-01
Morgan Deters
Merge pull request #44 from mdeters/prio-queue-updates
blob
|
commitdiff
|
raw
|
diff to current
2014-07-01
Morgan Deters
Merge pull request #45 from mdeters/turn-off-strings-exp
blob
|
commitdiff
|
raw
|
diff to current
2014-06-30
Kshitij Bansal
Merge pull request #47 from kbansal/sets
blob
|
commitdiff
|
raw
|
diff to current
2014-06-26
Morgan Deters
Merge tag 'smtcomp2014-resubmission'
blob
|
commitdiff
|
raw
|
diff to current
2014-06-25
Andrew Reynolds
Merge pull request #34 from mdeters/datatypes-kinds
blob
|
commitdiff
|
raw
|
diff to current
2014-06-25
Andrew Reynolds
Merge pull request #37 from mdeters/quants-kinds
blob
|
commitdiff
|
raw
|
diff to current
2014-06-25
Andrew Reynolds
Merge pull request #38 from mdeters/uf-kinds
blob
|
commitdiff
|
raw
|
diff to current
2014-06-25
Morgan Deters
Turn strings-exp off by default (for the release)
blob
|
commitdiff
|
raw
|
diff to current
2014-06-23
Morgan Deters
Fatal error if --unconstrained-simp and --produce-model...
blob
|
commitdiff
|
raw
|
diff to current
2014-06-22
Morgan Deters
Merge tag 'smtcomp2014-application'
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
lianah
fixed merge conflict
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
lianah
added model generation to eager bit-blasting and turned...
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
Morgan Deters
New translator features: expand define-funs and combine...
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
Morgan Deters
Fix for new CASC features, fixes Java builds.
blob
|
commitdiff
|
raw
|
diff to current
2014-06-19
ajreynol
For casc : print models of functions rewritten by sort...
blob
|
commitdiff
|
raw
|
diff to current
next