summaryrefslogtreecommitdiff
path: root/src/theory/bv
AgeCommit message (Collapse)Author
2012-06-13Fixed definition of bvsmodClark Barrett
2012-06-13Fixes more problems in bv rewritesClark Barrett
2012-06-13Fixes lots of problems in bv rewrite rules and adds lots of assertionsClark Barrett
to catch any that I may have missed
2012-06-12Changed bitvector theory rewriter so that equalities always get rewritten toClark Barrett
equalities or true or false
2012-06-11fixing bitvector bugsDejan Jovanović
* clauses shouldn't be erased when they could be a reason for outside propagation * propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally
2012-06-11OK, now the rewrite issues are fixedClark Barrett
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.
2012-06-11Fix for array bug with decision heuristicClark Barrett
Also fixed one bv rewrite failure (more to come)
2012-06-10Fixed one more bug in rewriterClark Barrett
2012-06-10Added a very fruitful assertion to the rewriter: checks that rewriting after ↵Clark Barrett
"REWRITE_DONE" is idempotent Found several problems where this is not the case and fixed them
2012-06-10fixes for bug347Dejan Jovanović
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ↵Dejan Jovanović
are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed
2012-05-31Fixed bug in bv: one more case where non-shared equality was getting propagatedClark Barrett
Added a global push and pop around solving - fixes an assertion failure when TNodes are still around in a CDHashMap at destruction time.
2012-05-30Added BitwiseEq bitvector rewriteClark Barrett
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times, twice before ite removal and twice after Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant speedup on dwp examples
2012-05-29Enabled SolveEq bv rewriteClark Barrett
2012-05-28Added some BV rewrites, fixed bugs in array theory, made ite simp work with BVClark Barrett
2012-05-27Committing the work on equality engine, I need to see how it does on the ↵Dejan Jovanović
regressions. New additions: * areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later. * propagation of shared dis-equalities (not yet complete, once case missing) * changes to the theories that use it, authors should check up on the changes
2012-05-24Separating the subtheory implementations in the bitvector theory.Dejan Jovanović
2012-05-21Updating equality manager to handle tagged trigger terms. Notifications are ↵Dejan Jovanović
pushed out for relationships between terms tagged with the same tag. No performance impact.
2012-05-17Fixed bug 338:Liana Hadarean
- fixed buggy rewrite rules assuming certain nodes only had 2 children - added support for bv-rewrite dump - fixed smt2_printer for bv constants
2012-05-16equality status for bitvectors can now look into the sat solver to check for ↵Dejan Jovanović
IN_MODEL status
2012-05-16refactored TheoryBV bitblaster and equality engine into subtheories (similar ↵Liana Hadarean
to TheoryEngine
2012-05-15fixed QF_BV performance problem due to using CDList instead of CDQueueLiana Hadarean
2012-05-15renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectivelyLiana Hadarean
2012-05-15fixing warnings, grrDejan Jovanović
2012-05-15several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify ↵Liana Hadarean
and now term notify handles boolean constants; fixed bug 328
2012-05-13fixing build warningsDejan Jovanović
2012-05-09* simplifying equality engine interfaceDejan Jovanović
* notifications are now through the interface subclass instead of a template * notifications include constants being merged * changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed * sat solver now has explicit methods to make true and false constants * 0-level literals are removed from explanations of propagations
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
This should also fix bug 325.
2012-05-03Some cleanup starting off from trying to understand the sharing code. ↵Dejan Jovanović
Changes include * fixed term visitor from the bvprop branch * removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles * moved the LogicInfo into the theory constructor
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-06processing assertions in bit-vectors even when in fullcheck (needed for sharing)Dejan Jovanović
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
* modified BVMinisat to work incrementally * added more bv regressions
2012-03-29Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function ↵Tim King
pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs.
2012-03-28fixed faulty bv rewrite ruleLiana Hadarean
2012-03-26More cleaning up.Dejan Jovanović
2012-03-25sat_module.h,cpp -> sat_solver.h,cpp (as intended)Dejan Jovanović
2012-03-22Merged updated version of the bitvector theory:Liana Hadarean
* added simplification rewrites
2012-03-02CDMap -> CDHashMapDejan Jovanović
CDSet -> CDHashSet
2012-02-29This should fix the debian build fails:Liana Hadarean
* removed bvpicosat directory as it is currently not used Cleared some of the flurry of warnings my previous merge caused in src/prop/
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
* separated SatSolverInput interface class into two classes: - TheoryProxy for the sat solver to communicate with the theories - SatSolverInterface abstract class to communicate with the sat solver * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces Replaced TheoryBV with bitblasting implementation: * all operators bitblasted * only operator elimination rewrite rules so far
2012-02-20portfolio mergeMorgan Deters
2011-12-08Disable a BV rewriter statistic (after checking with Liana) that was static,Morgan Deters
and thus caused big problems with programs that create two SmtEngines in one process. If we need state like this in the rewriters, we'll need to make them nonstatic.
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h>
2011-10-17Sharing workDejan Jovanović
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API This will need more work, but it's a start. Also implemented TheoryEngine::properPropagation(). Other minor things.
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-28variety of visibility fixes (should clean up some of the many warnings on ↵Morgan Deters
MacOS-production-dynamic builds)
2011-09-15additional stuff for sharing, Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback