cvc5.git
2015-08-25 ajreynolUse zero in cbqi when not using infinities.
2015-08-24 Liana HadareanAdded threshold for core bv cardinality lemmas
2015-08-24 Liana HadareanFix for bv core cardinality lemma generation
2015-08-24 Liana Hadareaneager bit-blasting gives models for boolean variables...
2015-08-24 ajreynolImprovements to vts in cbqi, bug fix vts for non-atomic...
2015-08-21 ajreynolMinor changes related to codatatypes for 1.5 release.
2015-08-21 ajreynolFix disequality bounds in cbqi, record literals for...
2015-08-20 Liana Hadareanfix to bug659 due to algebraic solver model building
2015-08-20 Liana Hadareanfix for bug660 and bug658 due to incorrect bit-blasting...
2015-08-19 ajreynolMake cbqi robust to term ITE removal. Separate vts...
2015-08-19 Kshitij Bansalfix bug 605
2015-08-19 ajreynolImplementation of model-based projection in cbqi, clean...
2015-08-18 Tianyi Liangfix for bug663
2015-08-16 ajreynolMore optimizations to --macros-quant, add --macros...
2015-08-12 ajreynolImprovements to --macros-quant. Enable --clause-split...
2015-08-01 ajreynolSimplification/improvement to solving deltas in LRA...
2015-08-01 ajreynolSupport for default grammar for datatypes in sygus...
2015-07-31 ajreynolMake --fmf-fun and --macros-quant work in incremental...
2015-07-31 ajreynolSygus support for inductive datatypes.
2015-07-30 ajreynolImplement virtual term substitution for non-nested...
2015-07-28 Tianyi LiangDisable bug590.smt2
2015-07-28 Tianyi Liangminor change to the last fix
2015-07-28 Tianyi LiangMerge branch 'master' of https://github.com/CVC4/CVC4
2015-07-28 Tianyi LiangHotfix for substr function.
2015-07-25 ajreynolAdd option --sygus-inv-templ for synthesizing strengthe...
2015-07-20 Tim KingFix for BOOST_SED_CPP for gcc-5.
2015-07-20 ajreynolSquashed merge of SygusComp 2015 branch.
2015-07-12 ajreynolAdd option --full-saturate-quant-rd. Fix option -...
2015-07-08 Kshitij Bansalfix bug 650
2015-07-05 ajreynolAdd options --partial-triggers, --elim-taut-quant,...
2015-07-02 ajreynolOn-demand upper bound lemmas for deltas in quantified...
2015-07-01 ajreynolAdd options --qcf-all-conflict, --ite-dtt-split-quant...
2015-06-30 Kshitij Bansalfix sets-translate
2015-06-30 Kshitij Bansalfix smt2 parameterized sort printing
2015-06-29 ajreynolModule to infer alpha equivalence of quantified formula...
2015-06-27 ajreynolRefactor various corner cases of fmf, quantifiers modul...
2015-06-25 ajreynolDo not assert fail for fmf empty domains. Fixes bug...
2015-06-22 ajreynolAdd --user-pat=interleave. Remove unused lte inst strategy.
2015-06-16 ajreynolAvoid completion for large finite types. Fix bug for...
2015-06-15 ajreynolMake array basis term a skolem (avoids crashing in...
2015-06-15 Clark BarrettChanging options for QF_AUFNIA to avoid bug
2015-06-14 Tim KingFixing an assertion Constraint::assertionFringe(.....
2015-06-14 Tim KingHanding the case in replay where a cut is directly...
2015-06-14 Tim KingFixes for shared term normalization in replay for const...
2015-06-13 Tim KingTurning off aggressive arith ite simplifications during...
2015-06-13 ajreynolRobust check to avoid store all instantiations. Fix...
2015-06-13 Tim KingChanging the run script for master for the application...
2015-06-13 Tim KingRestricting TheoryArith to computeRelevantTerms.
2015-06-13 ajreynolDisable sort inference for SMT COMP
2015-06-13 Clark BarrettFixed bug in iteSimp
2015-06-13 Clark BarrettFix for assertion failure:
2015-06-13 ajreynolFix for sort inference involving mixed Int/Real equalities.
2015-06-13 Tim KingA return value for an ApproxGLPK::loadVB() failure...
2015-06-13 ajreynolAvoid instantiating with array constants.
2015-06-13 ajreynolEnsure mkRep instantiation strategies do not violate...
2015-06-12 Kshitij Bansalsync options of default-assertions run script with...
2015-06-12 ajreynolFix crash in non-linear cbqi.
2015-06-12 Tim KingIn TheoryArithPrivate::vectorToIntHoleConflict, adding...
2015-06-12 ajreynolMake sygus an output language. Parse declare-fun in...
2015-06-12 ajreynolAccelerate sygus solution reconstruction for constants...
2015-06-11 Kshitij Bansalremove runscripts from master meant for experimental...
2015-06-11 ajreynolAvoid naming conflicts in sygus, refactor. Add missing...
2015-06-11 ajreynolHandle duplicate operators in sygus grammars. Parse...
2015-06-11 ajreynolUpdate experimental scripts. Support top-level non...
2015-06-10 ajreynolBug fix parsing constant constructor sygus.
2015-06-10 ajreynolSupport for printing solutions involving LetGTerm sygus...
2015-06-10 ajreynolParse support for sygus LetGTerm.
2015-06-09 Kshitij Bansalbump thread stack size to 1 GB
2015-06-09 ajreynolBug fix instantiations for fmf-bound-int. Disable...
2015-06-09 Kshitij Bansalmake comment precise
2015-06-09 Kshitij Bansalmove delete beyond ifdef CVC4_COMPETITION_MODE
2015-06-05 Kshitij Bansalpcvc4 with assertions
2015-06-05 Kshitij Bansalupdate run script for assertions/scrambled run
2015-06-05 Kshitij Bansalassertions runscript (for testing) derived from current...
2015-06-05 Kshitij Bansalfor experimental, use incremental instead of teardown...
2015-06-05 Kshitij Bansalmove decision to use teardown or not to logics
2015-06-04 ajreynolFix for last commit.
2015-06-04 Kshitij Bansalrpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtco...
2015-06-04 Kshitij Bansalsync exerimental scripts with regular ones
2015-06-04 ajreynolMinor changes to smt comp script for quantified arith...
2015-06-03 Kshitij Bansalexperimental run scripts
2015-06-03 Kshitij Bansalrunscript thread stack 256
2015-06-03 ajreynolRefactoring of sygus parsing, properly parse Constant...
2015-06-02 Kshitij Bansalapplication smtcomp
2015-06-02 ajreynolFlatten sygus grammars during parsing. Remove duplicate...
2015-06-02 ajreynolAdd casc 25 tfn script. Change tff script to output...
2015-06-01 ajreynolWhen proof enabled, disable uf sym break. Add regression.
2015-05-29 ajreynolDo not enforce dt fairness when single invocation sygus.
2015-05-29 lianahchanged resource step options to unsigned
2015-05-28 Liana Hadareanadded options for controlling resource step-count for...
2015-05-27 lianahMerge pull request #75 from Dunedune/master
2015-05-25 ajreynolAdd missing regression
2015-05-25 ajreynolBug fix for CNF proofs (and/or case 1), thanks to Alain...
2015-05-22 Jordy RuizAdded throw LogicException to method lemma.
2015-05-15 ajreynolFixes related to cbqi + E-matching.
2015-05-15 ajreynolAvoid ensureLiteral on unpreprocessed formulas in cbqi.
2015-05-13 ajreynolRefactor interface for incompleteness in quantifiers...
2015-05-12 Clark BarrettAdded Finn Haedicke as a contributor.
2015-05-12 barrettcwMerge pull request #74 from finnhaedicke/namespace_minisat
2015-05-11 ajreynolAllow sygus with no syntactic restrictions for LIA...
next