cvc5.git
2015-04-21 Tim KingAdding an example of a tester in SMT2.
2015-04-18 Tim KingFarkas proof coefficients.
2015-04-17 Tianyi LiangPatch for Kshitij's fix on requriePhase
2015-04-17 Kshitij BansalMerge pull request #72 from kbansal/decision-requirephase
2015-04-16 ajreynolFix option --quant-fun-wd. Add mk_starexec script...
2015-04-16 ajreynolHandle (degenerate) case of synthesis conjectures for...
2015-04-15 Tim KingEnabling the regression test: test/regress/regress0...
2015-04-15 Clark BarrettFix for unconstrained bug.
2015-04-15 Tim KingAdding an example that violates an assertion during...
2015-04-13 Tim KingMaking CVC4::theory::quantifiers::PrenexQuantMode publi...
2015-04-09 Kshitij Bansaldisable string reqressions timing out after change
2015-04-09 Kshitij BansalDE requests respect requirePhase
2015-04-09 ajreynolFix unsat-core issues related to rewrite rules, quantif...
2015-04-09 ajreynolFix performance issue with variable triggers + instanti...
2015-04-09 ajreynolBug fix negative contains cache.
2015-04-08 ajreynolMake fun-def quantifiers carry the function app they...
2015-04-08 Dejan JovanovicRemoving the reference to THEORY_BOOL from the equality...
2015-04-07 ajreynolMinor fixes for cegqi.
2015-04-02 Kshitij BansalMerge pull request #71 from kbansal/const-are-triggers
2015-04-01 ajreynolImprovements and bug fixes related to cbqi/cegqi. ...
2015-03-31 Kshitij Bansalfix no return value warning
2015-03-31 Kshitij Bansalfix echo command in --tear-down-incremental
2015-03-28 Tianyi Liangprinter change for string smtlib2
2015-03-25 Kshitij Bansalchange const are triggers from false to true in equalit...
2015-03-23 ajreynolParsing support for define-fun-rec/define-funs-rec.
2015-03-23 ajreynolDecouple counter-example guided quantifier instantiatio...
2015-03-16 Tianyi LiangAdd requirePhase len(x) = 0.
2015-03-16 Liana HadareanFixed proof unitialized memory and minor memory leaks.
2015-03-14 Tianyi LiangBug fix for BV
2015-03-14 Tianyi LiangPatches for 32-bit ARM
2015-03-14 Dejan JovanovicUpdating resize for occurence lists to properly resize...
2015-03-11 ajreynolStrings split on constant lengths, add length=0 to...
2015-03-11 ajreynolMinor fixes and improvements to cegqi-si for linear...
2015-03-10 ajreynolCNF proofs. Infrastructure for preprocessing proofs...
2015-03-05 ajreynolMinor fixes. Extend cegqi-si to real arithmetic.
2015-03-04 ajreynolMore work on arithmetic single invocation synthesis...
2015-02-28 Kshitij BansalRevert "dummy commit to force nightly builds"
2015-02-26 ajreynolRobust strategy for single invocation LIA synthesis...
2015-02-25 Tianyi LiangSwitch back to eager loop temporarily.
2015-02-25 Tianyi Liangminor fix for internal string print
2015-02-22 ajreynolNew trigger options. --inst-no-entail on by default...
2015-02-19 Kshitij Bansaldummy commit to force nightly builds
2015-02-16 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4
2015-02-16 Kshitij Bansalwebget: curl follow redirect
2015-02-14 ajreynolFix unit tests.
2015-02-14 Kshitij Bansalattempt to fix win32 builds
2015-02-13 ajreynolMinor cleanup, remove unused files.
2015-02-13 ajreynolHandle recursive singleton case for codatatypes, add...
2015-02-12 Kshitij Bansaltry curl before wget, workaround for issue with FTP...
2015-02-12 Tim KingChanging CXXFLAGS for custom cln installation in config...
2015-02-11 ajreynolBetter support for solving multiple functions with...
2015-02-11 ajreynolMove si solution reconstruction to own file, make more...
2015-02-06 ajreynolHandle missing cases for single inv solution reconstruc...
2015-02-06 Tianyi LiangMinor clean up
2015-02-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2015-02-06 Tianyi LiangImproved string performance, thanks to Peter's benchmarks.
2015-02-06 Tianyi LiangImproved string performance, thanks to Peter's benchmarks.
2015-02-05 ajreynolWorking version of sygus solution reconstruction from...
2015-02-04 ajreynolInitial draft of solution reconstruction into syntax...
2015-02-04 ajreynolWork on solution reconstruction for single inv. Fix...
2015-02-04 ajreynolRefactor sygus_util to TermDb. Initial work on solutio...
2015-02-04 ajreynolStart work on simplifying single inv solutions. Minor.
2015-02-03 ajreynolSimple variable elimination for single inv properties...
2015-02-02 ajreynolSolutions for single invocation conjectures.
2015-02-02 ajreynolSingle invocation module for counterexample guided...
2015-02-02 ajreynolRepresentative programs must be minimal size, minor...
2015-02-01 ajreynolGeneralization of sygus lemmas based on arguments and...
2015-01-31 ajreynolBug fix fairness for commutative operators in sygus...
2015-01-31 ajreynolLemmas instead of conflicts in sygus sym break (do...
2015-01-30 ajreynolGeneralize conflict clauses in sygus sym break, merge...
2015-01-29 ajreynolApply sygus search space narrowing for all subprograms...
2015-01-29 ajreynolRestrict LtePartialInst instantiations based on E-match...
2015-01-29 ajreynolApply global search space narrowing for multiple synth...
2015-01-29 ajreynolAdd module for sygus search space narrowing based on...
2015-01-28 ajreynolMinor refactor CEGQI.
2015-01-27 ajreynolAlways miniscope nested quantifiers. Disable miniscopi...
2015-01-27 ajreynolRecognize when synthesis conjectures are in single...
2015-01-26 ajreynolOutput solutions for synthesis conjectures with --dump...
2015-01-26 ajreynolGeneralize sygus search space narrowing to arbitrary...
2015-01-24 ajreynolVariable patterns only look at eligible terms. Minor...
2015-01-24 ajreynolAdd --lte-restrict-inst-closure option. Push dt.size...
2015-01-23 ajreynolRefactor sygus arg nf. Minor improvements.
2015-01-23 ajreynolCEGQI fairness based on term height. Fix sygus-nf...
2015-01-23 ajreynolRework inst-closure.
2015-01-22 ajreynolNarrow sygus search space based on NNF and rewriting...
2015-01-22 ajreynolAdd option --lte-partial-inst. Remove inst-closure.
2015-01-22 ajreynolDo not drop patterns during boolean term rewriting...
2015-01-21 ajreynolAvoid redundant constant arguments for SygusNormalForm...
2015-01-21 ajreynolInitial work on sygusNormalForm.
2015-01-20 ajreynolMark datatypes as sygus. Add option to normalize sygus...
2015-01-20 ajreynolHandle miniscoping of conjunctions in synthesis propert...
2015-01-19 Tim KingAdding tests for get-value output for arithmetic.
2015-01-19 Tim KingAdding an additional search path to configure.ac for...
2015-01-17 ajreynolAvoid name conflicts for multiple synth-fun.
2015-01-16 ajreynolLinearize multiplication by constants in sygus grammars...
2015-01-16 ajreynolAllow uninterpreted/defined functions in Sygus grammars...
2015-01-16 ajreynolMinor: Ensure indexed terms are in EE. Add support...
2015-01-14 Morgan Deterssygus input language and benchmark
2015-01-13 Morgan DetersFix #line numbering.
2015-01-13 Morgan DetersFix a memory issue in ResourceManager on 32-bit (resolv...
next