| 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 |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup.
|
commit | commitdiff | tree |
| 2010-09-24 |
Dejan Jovanović | equality triggers for the equality engine
|
commit | commitdiff | tree |
| 2010-09-24 |
Dejan Jovanović | basic union find for bitvectors
|
commit | commitdiff | tree |
| 2010-09-21 |
Dejan Jovanović | iterators for tim, begin<PLUS>() and end<PLUS>() should...
|
commit | commitdiff | tree |
| 2010-09-20 |
Dejan Jovanović | hooking up the bitvector tests
|
commit | commitdiff | tree |
| 2010-09-20 |
Dejan Jovanović | bitvector rewriting for the core theory and testcases
|
commit | commitdiff | tree |
| 2010-08-20 |
Dejan Jovanović | updating the minisat restart parameters after running...
|
commit | commitdiff | tree |
| 2010-08-16 |
Dejan Jovanović | Fixing failures in minisat
|
commit | commitdiff | tree |
| 2010-08-15 |
Dejan Jovanović | (no commit message)
|
commit | commitdiff | tree |
| 2010-08-15 |
Dejan Jovanović | (no commit message)
|
commit | commitdiff | tree |
| 2010-08-13 |
Dejan Jovanović | renaming minisat .C to .cc
|
commit | commitdiff | tree |
| 2010-08-13 |
Dejan Jovanović | Adding the changes to the original copy
|
commit | commitdiff | tree |
| 2010-07-10 |
Dejan Jovanović | Fix for the type in sat propagation.
|
commit | commitdiff | tree |
| 2010-07-09 |
Dejan Jovanović | the tableaux optimization
|
commit | commitdiff | tree |
| 2010-06-01 |
Dejan Jovanović | In order for splitting on demand to be able to retract...
|
commit | commitdiff | tree |
| 2010-05-25 |
Dejan Jovanović | Some initial changes to allow for lemmas on demand.
|
commit | commitdiff | tree |
| 2010-05-06 |
Dejan Jovanović | fixing the nightly failure. TypeCheckingException is...
|
commit | commitdiff | tree |
| 2010-05-05 |
Dejan Jovanović | changing the interface to bit-vector constant constructor
|
commit | commitdiff | tree |
| 2010-05-05 |
Dejan Jovanović | bit-vector constant constructor from string
|
commit | commitdiff | tree |
| 2010-05-05 |
Dejan Jovanović | bug fixes for types, old unit tests for types work now
|
commit | commitdiff | tree |
| 2010-05-04 |
Dejan Jovanović | Type-checking classes and hooks (not tested yet).
|
commit | commitdiff | tree |
| 2010-05-02 |
Dejan Jovanović | smt parser for bit-vectors
|
commit | commitdiff | tree |
| 2010-05-01 |
Dejan Jovanović | Fix for the last night's build errors (type that broke...
|
commit | commitdiff | tree |
| 2010-04-30 |
Dejan Jovanović | Fix for bug 115, mapping was going in the wrong direction.
|
commit | commitdiff | tree |
| 2010-04-29 |
Dejan Jovanović | Added the capability to construct expressions by passing...
|
commit | commitdiff | tree |
| 2010-04-28 |
Dejan Jovanović | adding integer and real types to the public interface
|
commit | commitdiff | tree |
| 2010-04-28 |
Dejan Jovanović | Build fix for parser
|
commit | commitdiff | tree |
| 2010-04-26 |
Dejan Jovanović | Some cleanup. Also added the integer and real types.
|
commit | commitdiff | tree |
| 2010-04-26 |
Dejan Jovanović | Adding the intermediary TypeNode to represent (and...
|
commit | commitdiff | tree |
| 2010-04-15 |
Dejan Jovanović | Adding info in the minisat README
|
commit | commitdiff | tree |
| 2010-04-14 |
Dejan Jovanović | Marging from types 404:415, changes: Massive
|
commit | commitdiff | tree |
| 2010-03-12 |
Dejan Jovanović | Fixing unnecessary construction of NOT nodes when...
|
commit | commitdiff | tree |
| 2010-03-11 |
Dejan Jovanović | Changing const TNode& to TNode in the CNF conversion...
|
commit | commitdiff | tree |
| 2010-03-11 |
Dejan Jovanović | Boolean variables were marked as theory literals by...
|
commit | commitdiff | tree |
| 2010-03-11 |
Dejan Jovanović | Fix for the main bug that was bugging me -- Bug 49...
|
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | Adding the smallest of test cases from the smtlib.
|
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | removing makefile.in
|
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | one more simple test for uf
|
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | (no commit message)
|
commit | commitdiff | tree |
| 2010-03-08 |
Dejan Jovanović | adding simple-uf to the regressions, and the code that...
|
commit | commitdiff | tree |
| 2010-03-08 |
Dejan Jovanović | Fixing Debug("prop") => Debug("node") typo
|
commit | commitdiff | tree |
| 2010-03-08 |
Dejan Jovanović | some more sat stuff for tim: assertions now go to theory_uf
|
commit | commitdiff | tree |
| 2010-03-08 |
Dejan Jovanović | Adding quiet output of make by default. There are two...
|
commit | commitdiff | tree |
| 2010-03-04 |
Dejan Jovanović | Adding phase-caching to minisat.
|
commit | commitdiff | tree |
| 2010-03-03 |
Dejan Jovanović | Some SAT stuff, not doing anything special yet, just...
|
commit | commitdiff | tree |
| 2010-02-28 |
Dejan Jovanović | * context.h - Changed cdlist::push_back to use a new...
|
commit | commitdiff | tree |
| 2010-02-26 |
Dejan Jovanović | Changing the hashing in attributes to what Nodes do...
|
commit | commitdiff | tree |
| 2010-02-23 |
Dejan Jovanović | cosmetic changes, comments, and renaming of Expr related...
|
commit | commitdiff | tree |
| 2010-02-22 |
Dejan Jovanović | finally works
|
commit | commitdiff | tree |
| 2010-02-22 |
Dejan Jovanović | Merging from branch branches/Liana r241
|
commit | commitdiff | tree |
| 2010-02-22 |
Dejan Jovanović | Small changes to the smt-engine, removed the assertions...
|
commit | commitdiff | tree |
| 2010-02-16 |
Dejan Jovanović | removing assertion and warning that shouldn't be there...
|
commit | commitdiff | tree |
| 2010-02-13 |
Dejan Jovanović | simplification minisat
|
commit | commitdiff | tree |
| 2010-02-13 |
Dejan Jovanović | Improvements to CNF conversion when already in CNF
|
commit | commitdiff | tree |
| 2010-02-12 |
Dejan Jovanović | build fix
|
commit | commitdiff | tree |
| 2010-02-12 |
Dejan Jovanović | Fix to compile out Debug(...) << ... statements in...
|
commit | commitdiff | tree |
| 2010-02-12 |
Dejan Jovanović | Changes to hashing that solve the xinetd boolean benchmark...
|
commit | commitdiff | tree |
| 2010-02-11 |
Dejan Jovanović | svn ignore
|
commit | commitdiff | tree |
| 2010-02-10 |
Dejan Jovanović | fixing annoying eclipse build settings, no more broken...
|
commit | commitdiff | tree |
| 2010-02-09 |
Dejan Jovanović | Changes to the CNF conversion and the SAT solver. All...
|
commit | commitdiff | tree |
| 2010-02-09 |
Dejan Jovanović | empty stubs for push and pop to fix the build fail
|
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Disabling the failing test case for the context.
|
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Fixing the test case, it had a unary or. The cnf converter...
|
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Push/Pop parsing and commands
|
commit | commitdiff | tree |
| 2010-02-08 |
Dejan Jovanović | Moving the template stuff back into the header in order...
|
commit | commitdiff | tree |
| 2010-02-04 |
Dejan Jovanović | beautification of the prop engine
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search