cvc5.git
2013-04-30 lianahadded several rewrite rules (BitwiseSlicing, Ule/SleEli...
2013-04-30 lianahadded bvule, bvsle operator elimination rulesl; added...
2013-04-30 lianahadded some bv rewrite rules
2013-04-30 lianahinnd examples are solved fast, but destruction assertio...
2013-04-30 Liana Hadareanfixed compile error
2013-04-30 lianahuncompiling new bv to bool lifting
2013-04-30 lianahfinished implementing bv to bool lifting and added...
2013-04-30 Liana Hadareanmore work on boolean lifting
2013-04-30 lianahstarted work on bv1 to boolean lifting
2013-04-30 lianahadded support for dumping the SAT problem the sat solve...
2013-04-30 Andrew ReynoldsAdd option in quantifiers for clause splitting
2013-04-30 Kshitij Bansaladd decision_attributes.h for make dist
2013-04-29 Morgan DetersSome fixes for GCC 4.2, and for Java on Mac
2013-04-29 Kshitij BansalMerge pull request #9 from kbansal/master
2013-04-29 Morgan DetersFixes to FCSimplex for some versions of compilers
2013-04-28 Tim KingFixing the failure for make distcheck.
2013-04-26 Kshitij BansalMerge experimental decisionweight branch
2013-04-26 Tim KingFCSimplex branch merge
2013-04-25 Morgan DetersAdd ability to run different regression levels with...
2013-04-24 Morgan DetersTheory "alternates" support
2013-04-22 Morgan Detersadd bit0 and bit1 constants to smt-lib v1 parser
2013-04-18 lianahmaking sure sat context is zero when user context is...
2013-04-18 lianahfixing destruction order in SmtEngine
2013-04-17 Kshitij Bansalbool flatten: node num_children workaround
2013-04-17 Kshitij Bansalboolean flatten: bug fix in dfs search
2013-04-17 Kshitij Bansalboolean flatten rewrite: dont re-rewrite
2013-04-17 Kshitij Bansalgeneralize to handle and
2013-04-16 Kshitij Bansalflatten or nodes
2013-04-11 Clark BarrettImproved speed of no redundant lemma assertion by using...
2013-04-11 Clark BarrettFixes for getModelVal in bv theory
2013-04-11 Clark BarrettAdded check for infinite lemma loop
2013-04-11 lianahfixed getModelValue to only query the value of leaves...
2013-04-09 Morgan DetersChange TPTP parser to not use the STRING type; this...
2013-04-05 Morgan DetersFix unit test (compile error) for new SatSolver interface
2013-04-03 Dejan Jovanović* changing the bitblast-eager to bitblast on pre-register
2013-04-03 Morgan DetersPrerelease versioning for master.
2013-04-03 Morgan DetersPre-release versioning
2013-04-03 Morgan DetersCutting release 1.1.
2013-04-03 Morgan DetersSome final minor changes before cutting 1.1.
2013-04-03 Liana Hadareanupdated NEWS to include inequality solver
2013-04-03 Andrew Reynoldsabort quantifiers check if master equality engine is...
2013-04-02 Tim KingMaking arithmetic model reversion on unsat checks an...
2013-04-02 Morgan DetersRegenerated copyrights: canonicalized names, no emails
2013-04-02 Morgan DetersRemove old README file from rewrite-rules left over...
2013-04-02 Morgan DetersFix get-authors script to not extract email addresses...
2013-04-02 Morgan DetersOne final fix to "make submission" rule
2013-04-02 Morgan Detersupdate copyrights
2013-04-02 Morgan DetersAdjust release Makefile rules, new run script
2013-04-02 Clark BarrettFix regression error by turning off model-based solver...
2013-04-02 Clark BarrettTurning on model based array solver for QF_AX
2013-04-02 Clark BarrettMade eager lemmas an option, enabled for QF_AX
2013-04-02 Clark BarrettDisabling eager array index splitting for QF_AX
2013-04-02 Morgan DetersFixes for two bugs:
2013-04-01 Tim KingCleaning up the demand restart code.
2013-04-01 Tim KingAdding a restart test strategy to integers.
2013-04-01 Tim KingAdding demand restart.
2013-04-01 Tim KingAdding tests for the previous commit.
2013-04-01 Morgan DetersMerging some cleanup work:
2013-04-01 Tim KingFix for iff terms over equalities between the same...
2013-04-01 Morgan DetersFix bug 491 and related issues with checkModel() and...
2013-04-01 lianahfixed TheoryBool rewriter bug
2013-04-01 lianahfixed bug 502; now the core bv solver only gives the...
2013-03-31 Liana Hadareanchanged option to run inequality solver by default
2013-03-31 Clark BarrettDisabling eager array index splitting for QF_AUFLIA
2013-03-30 Andrew Reynoldsdo simple ite rewriting within quantifiers
2013-03-29 Morgan Detersmake Boolean term conversion partially non-recursive...
2013-03-29 Dejan JovanovićMerge branch 'master' of github.com:CVC4/CVC4
2013-03-29 Dejan Jovanovićremoving cryptominisat since we're not using it
2013-03-28 Morgan Detersfix memory corruption in arrays destructor
2013-03-28 Morgan Deterssome Java bindings fixes (fixes Debian build problems)
2013-03-28 Clark BarrettFixed a warning, made eager-index default to true ...
2013-03-28 Clark BarrettFixed bug in arrays
2013-03-28 Clark BarrettAdded assertion
2013-03-28 Clark BarrettUpdates to model-based array solver
2013-03-28 Clark BarrettNew model-based array procedure
2013-03-27 lianahreverted the core solver to do static slicing, added...
2013-03-27 lianahfixed inequality checkDisequalities inefficiency
2013-03-27 lianahMerge branch 'master' into bv-core
2013-03-27 lianahfixed some model stuff
2013-03-27 lianahfixed model generation bug; commented out attempt...
2013-03-27 lianahinequality solver now only splits on disequalities...
2013-03-27 lianahadded model generation for bv subtheories and bv-inequa...
2013-03-26 Morgan DetersFixes for warnings from clang++, from -std=gnu++0x...
2013-03-26 Morgan DetersMake --incremental the default when running interactively
2013-03-26 lianahcore theory currently disabled
2013-03-26 Dejan JovanovićgetModelValue implementation in bitvectors
2013-03-26 Dejan Jovanovićadding
2013-03-26 Dejan JovanovićMerge branch 'master' of git@github.com:CVC4/CVC4.git
2013-03-26 Dejan Jovanovićmoving bv before arrays
2013-03-26 lianahfixed inequality bugs due to improper explanation
2013-03-26 lianahcleaned up the bv subtheory interface; added check...
2013-03-26 Morgan Detersjava input stream adapters working
2013-03-25 lianahgetEqualityStatus now also queries the inequality solver
2013-03-25 Morgan DetersFix for SCM detection
2013-03-25 Kshitij BansalMerge pull request #7 from kbansal/portfolio
2013-03-25 Kshitij Bansalfinish removal of separateOutput
2013-03-25 Liana Hadareanadded support for disequalities in the inequality solver
2013-03-24 lianahincremental inequality solver implemented
2013-03-24 Morgan DetersFix bug in portfolio executor output; fixes nightly...
2013-03-23 lianahnon-incremental inequality solver seems to be bug-free...
next