| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand...
|
commit | commitdiff | tree |
| 2012-04-18 |
Dejan Jovanović | disabling the problematic pragma in node_manager.h...
|
commit | commitdiff | tree |
| 2012-04-17 |
Dejan Jovanović | Fix for thos annoying "array index" warnings in production...
|
commit | commitdiff | tree |
| 2012-04-06 |
Dejan Jovanović | processing assertions in bit-vectors even when in fullcheck...
|
commit | commitdiff | tree |
| 2012-04-04 |
Dejan Jovanović | some settings in bvminisat
|
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | some more build system fixes
|
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | fixing some build systme warnings
|
commit | commitdiff | tree |
| 2012-03-29 |
Dejan Jovanović | bringing cryptominisat into the main branch
|
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | enabling the --disable-arithmetic-propagation option...
|
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | Some renaming and refactoring in SAT
|
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | getting rid of a rewrite in uf sharing, speeds things...
|
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | adding an extra cache check in the rewriter, speeds...
|
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | Global registry of SAT solvers, where they are registered...
|
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | More cleaning up.
|
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | more datail from the build failure
|
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | with a small fix
|
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | forgot to commit this one, fixing build errors
|
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | moving minisat implementation into their respective...
|
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat_module.h,cpp -> sat_solver.h,cpp (as intended)
|
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)
|
commit | commitdiff | tree |
| 2012-03-24 |
Dejan Jovanović | a cute script to make a video of development from the...
|
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | * improving arithmetic getEqualityStatus
|
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | some improvements to the sharing mechanism/interface
|
commit | commitdiff | tree |
| 2012-03-08 |
Dejan Jovanović | Fixin the bug Clark found. In final check, enqueued...
|
commit | commitdiff | tree |
| 2012-03-08 |
Dejan Jovanović | Removing QUICK_CHECK, and other unused ones, from the...
|
commit | commitdiff | tree |
| 2012-03-06 |
Dejan Jovanović | updating the equality engine to be able to give explanations...
|
commit | commitdiff | tree |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap
|
commit | commitdiff | tree |
| 2012-02-29 |
Dejan Jovanović | fixing bug310
|
commit | commitdiff | tree |
| 2012-02-25 |
Dejan Jovanović | ppAsert -> ppAssert
|
commit | commitdiff | tree |
| 2012-02-24 |
Dejan Jovanović | Theory interface changes:
|
commit | commitdiff | tree |
| 2012-02-21 |
Dejan Jovanović | Fix for bug303. The problem was with function applications...
|
commit | commitdiff | tree |
| 2012-02-09 |
Dejan Jovanović | fixing antoher small bug in backtracking
|
commit | commitdiff | tree |
| 2012-02-08 |
Dejan Jovanović | fixing a bug in uf_engine application lookup backtracking
|
commit | commitdiff | tree |
| 2012-02-07 |
Dejan Jovanović | removing the 100 integer benchmarks from regress0,...
|
commit | commitdiff | tree |
| 2012-02-07 |
Dejan Jovanović | fixing some missing stuff
|
commit | commitdiff | tree |
| 2012-02-05 |
Dejan Jovanović | changes to the cvc4 language printer, so that it actually...
|
commit | commitdiff | tree |
| 2012-02-03 |
Dejan Jovanović | updating configure to use python-config for building...
|
commit | commitdiff | tree |
| 2012-01-23 |
Dejan Jovanović | fix for bug295
|
commit | commitdiff | tree |
| 2011-12-14 |
Dejan Jovanović | some more bug fixes (TNode -> Node, normalize literals...
|
commit | commitdiff | tree |
| 2011-12-12 |
Dejan Jovanović | * merging some uf stuff from incremental_work branch...
|
commit | commitdiff | tree |
| 2011-12-10 |
Dejan Jovanović | adding additional checks for theories propagating literals...
|
commit | commitdiff | tree |
| 2011-12-10 |
Dejan Jovanović | a bit more changes, when propagting equalities/dis...
|
commit | commitdiff | tree |
| 2011-12-10 |
Dejan Jovanović | attempt to fix bug 293: if a split on a trivial shared...
|
commit | commitdiff | tree |
| 2011-10-17 |
Dejan Jovanović | Sharing work
|
commit | commitdiff | tree |
| 2011-09-15 |
Dejan Jovanović | tim's fixes for context-dependent pre-registration
|
commit | commitdiff | tree |
| 2011-09-15 |
Dejan Jovanović | adding --show-debug-tags to list all available debug...
|
commit | commitdiff | tree |
| 2011-09-15 |
Dejan Jovanović | additional stuff for sharing,
|
commit | commitdiff | tree |
| 2011-09-07 |
Dejan Jovanović | fixes for uf/equality engine from the quantifiers branch...
|
commit | commitdiff | tree |
| 2011-09-03 |
Dejan Jovanović | removing an assert i forgot to remove that andy found
|
commit | commitdiff | tree |
| 2011-09-02 |
Dejan Jovanović | * Changing pre-registration to be context dependent...
|
commit | commitdiff | tree |
| 2011-08-30 |
Dejan Jovanović | Fixin the SAT solver for Andy. Even if a SAT lemma...
|
commit | commitdiff | tree |
| 2011-08-27 |
Dejan Jovanović | Removing Theory::registerTerm() as discussed in the...
|
commit | commitdiff | tree |
| 2011-08-25 |
Dejan Jovanović | Fixing the broken unit tests
|
commit | commitdiff | tree |
| 2011-08-24 |
Dejan Jovanović | Simplification of the preregister and register throught...
|
commit | commitdiff | tree |
| 2011-08-23 |
Dejan Jovanović | some uf cleanup
|
commit | commitdiff | tree |
| 2011-08-17 |
Dejan Jovanović | new implementation of lemmas on demand
|
commit | commitdiff | tree |
| 2011-07-11 |
Dejan Jovanović | adding disequality propagation
|
commit | commitdiff | tree |
| 2011-07-10 |
Dejan Jovanović | changing the sat solver remove clauses constants
|
commit | commitdiff | tree |
| 2011-07-10 |
Dejan Jovanović | another typo
|
commit | commitdiff | tree |
| 2011-07-10 |
Dejan Jovanović | yet another uf bug fix, hopefully the last
|
commit | commitdiff | tree |
| 2011-07-10 |
Dejan Jovanović | another bugfix for uf
|
commit | commitdiff | tree |
| 2011-07-09 |
Dejan Jovanović | some immediate bug fixes
|
commit | commitdiff | tree |
| 2011-07-09 |
Dejan Jovanović | surprize surprize
|
commit | commitdiff | tree |
| 2011-07-07 |
Dejan Jovanović | removing duplicate clauses in ite cnf conversion
|
commit | commitdiff | tree |
| 2011-07-06 |
Dejan Jovanović | Fixing two bugs:
|
commit | commitdiff | tree |
| 2011-07-05 |
Dejan Jovanović | missing test case
|
commit | commitdiff | tree |
| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities...
|
commit | commitdiff | tree |
| 2011-05-02 |
Dejan Jovanović | updating bv regressions
|
commit | commitdiff | tree |
| 2011-05-02 |
Dejan Jovanović | parser fixes for bug 243
|
commit | commitdiff | tree |
| 2011-05-02 |
Dejan Jovanović | updates for bitvectors
|
commit | commitdiff | tree |
| 2011-04-14 |
Dejan Jovanović | reverting back the minisat code and adding a simpler...
|
commit | commitdiff | tree |
| 2011-04-14 |
Dejan Jovanović | fixing an uninitialized literal variable
|
commit | commitdiff | tree |
| 2011-04-13 |
Dejan Jovanović | adding support for unit conflicts in minisat...
|
commit | commitdiff | tree |
| 2011-04-09 |
Dejan Jovanović | changing the sat solver to assert propagated literals...
|
commit | commitdiff | tree |
| 2011-03-30 |
Dejan Jovanović | adding CVC4:: qualifier to the #define for debugging...
|
commit | commitdiff | tree |
| 2011-03-26 |
Dejan Jovanović | fix for bug 253, was propagating an asserted literal
|
commit | commitdiff | tree |
| 2011-03-22 |
Dejan Jovanović | updating debug output usage to eliviate impact of bug 252
|
commit | commitdiff | tree |
| 2011-03-21 |
Dejan Jovanović | more bugfixes, some basic propagation, and testcases...
|
commit | commitdiff | tree |
| 2011-03-21 |
Dejan Jovanović | fixing a bug in the BV rewrite, off by one error when...
|
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | again a typo
|
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | more bugfixes for bitvectors
|
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | fixing the failure from last nigth, due to using a...
|
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | missed one case
|
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | commit for the version of bitvectors that passes all...
|
commit | commitdiff | tree |
| 2011-03-17 |
Dejan Jovanović | push and pop manipulators for output stream so that...
|
commit | commitdiff | tree |
| 2011-03-15 |
Dejan Jovanović | real fix for bug 245, previous one was faulty
|
commit | commitdiff | tree |
| 2011-03-15 |
Dejan Jovanović | fix for bug 254, lemmas were propagating at lower levels...
|
commit | commitdiff | tree |
| 2011-03-14 |
Dejan Jovanović | adding support for google performance tools to the...
|
commit | commitdiff | tree |
| 2011-03-03 |
Dejan Jovanović | fixing a type that caused the segfaults in the regressions
|
commit | commitdiff | tree |
| 2011-03-02 |
Dejan Jovanović | fixing the big with lemma reallocation in minisat garbage...
|
commit | commitdiff | tree |
| 2011-02-26 |
Dejan Jovanović | adding the variables count to the statistics in the...
|
commit | commitdiff | tree |
| 2011-02-26 |
Dejan Jovanović | adding statistics about how many different kinds of...
|
commit | commitdiff | tree |
| 2011-02-25 |
Dejan Jovanović | slicing manager is not breaking the old regressions...
|
commit | commitdiff | tree |
| 2011-02-17 |
Dejan Jovanović | some unit tests to work on slicing
|
commit | commitdiff | tree |
| 2011-02-17 |
Dejan Jovanović | getting ready for slicing bitvectors
|
commit | commitdiff | tree |
| 2011-02-16 |
Dejan Jovanović | updates for the rewriter, added some statistics
|
commit | commitdiff | tree |
| 2011-01-05 |
Dejan Jovanović | fix for build errors
|
commit | commitdiff | tree |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes....
|
commit | commitdiff | tree |
| 2010-11-24 |
Dejan Jovanović | Changin the get() semantics to a CDQeue-sque semantics.
|
commit | commitdiff | tree |
| 2010-11-12 |
Dejan Jovanović | Some bug fixes in the SAT for lemmas, and an experiment...
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search