summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.h
AgeCommit message (Collapse)Author
2013-04-03* changing the bitblast-eager to bitblast on pre-registerDejan Jovanović
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate) * when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true) * bitblast-eager implies decision=internal
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ↵Tim King
CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
2012-11-26fixup for incremental solvingDejan Jovanović
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ↵Morgan Deters
\file tags corrected, copyright added to files that had it missing, etc. I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
2012-03-25sat_module.h,cpp -> sat_solver.h,cpp (as intended)Dejan Jovanović
2012-03-25sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)Dejan Jovanović
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
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-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in ↵Morgan Deters
my previous checkin)
2012-02-20portfolio mergeMorgan Deters
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵Morgan Deters
to model gen on booleans; and a little cleanup
2011-09-30fixes to incremental simplification, cnf routines, other stuff in ↵Morgan Deters
preparation of user push/pop in SAT solver
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-08-17new implementation of lemmas on demandDejan Jovanović
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-04-10merge from replay branchMorgan Deters
2011-04-05Minor adjustments to the Registrar commit in 1644, documentation.Morgan Deters
2011-04-04Merging the satliteral-before-prereg branch into trunk. Theory ↵Tim King
preregistration is now called during the conversion to cnf. This fixes bug 257.
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some ↵Morgan Deters
documentation, and make it possible to "make doc" on a clean source tree (post-configure)
2010-10-09Model generation for arith, boolean, and uf theories viaMorgan Deters
(get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec, you must pass --interactive --produce-models on the command line (although they don't currently make us do any extra work). Closes bug #213.
2010-08-16Fixing failures in minisatDejan Jovanović
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-06-29Merging the unate-propagator branch into the trunk. This is a big update so ↵Tim King
expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
** file-level documentation at the top of the sources. ** This is the "make bugzilla stop bugging me" bugfix commit. * Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy. Updated documentation in the file. Resolves bug #99. * Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.) moved into a separate file. Partially resolves bug #100. * Moved isAssociative(Kind) into kind.h (and into the CVC4::kind namespace) instead of metakind.h (where it was in CVC4::metakind). This clears up a warning (private #inclusion) from the SMT and SMT2 parsers, and maybe makes more sense anyways, since this is based on the kind (and not the metakind) of an operator. * Documentation improvement; doxygen top-level \file gestures, \brief gestures for files, etc. Changed contrib/update-copyright.pl for this change, and post-processed to add \brief. Resolves bug #98. * Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind). They no longer made sense. Resolves bug #91.
2010-06-01In order for splitting on demand to be able to retract clauses every ↵Dejan Jovanović
translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ↵Tim King
to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.
2010-05-25Some initial changes to allow for lemmas on demand. Dejan Jovanović
To be done: * Add erasable map Clause* to bool to minisat (backtracks with the solver) * Add map from Clause* to Node (clauses that came from a node) * Add reference counting Literal -> Node to CNFManager * If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable) * If clause is erased for each L in clause L -> Node refcount goes down
2010-05-14Adding debugging code in PropEngine/CnfStreamChristopher L. Conway
2010-05-14Adding rudimentary ITE handling in CnfStreamChristopher L. Conway
2010-05-14Virtualizing interface between CnfStream and SatSolverChristopher L. Conway
2010-05-13Minor refactorings and corrections to commentsChristopher L. Conway
2010-04-01reran update-copyright.pl to get new contributors and add new header ↵Morgan Deters
comments to files without them
2010-03-25Adding comments to NodeManagerChristopher L. Conway
Minor name changes for cleanup and hash function templates
2010-03-11Changing const TNode& to TNode in the CNF conversion + a new small benchmark ↵Dejan Jovanović
that fail on "x != x"
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
2010-03-08some more sat stuff for tim: assertions now go to theory_uf Dejan Jovanović
2010-03-02* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"Morgan Deters
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for NodeBuilder in certain cases * (various places) don't overload __gnu_cxx::hash<>, instead provide an explicit hash function to hash_maps and hash_sets. * add a new kind of assert, DtorAssert(), which doesn't throw exceptions (right now it operates like a usual C assert()). For use in destructors. * don't import NodeValue into CVC4 namespace (leave under CVC4::expr::). * fix some Make rule dependencies * reformat node.h as per code formatting policy * added Theory and NodeBuilder unit tests
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
test behavior of grow(), which was previously very broken, fixed by Tim earlier this afternoon. * add the notion of a "private header". Private header files (those not intended for distribution) should now #include "cvc4_private.h" (or "cvc4parser_private.h" for the parser code). When not actually building libcvc4 (resp. libcvc4parser), or associated unit tests, a warning is emitted by the preprocessor. This should make it easier to notice (and disentangle early) any unwanted public/private mixing. Currently the warning identifies a couple places where we need to fix things. * added directory infrastructure for arrays and BV theories. * the Theory inheritance hierarchy makes some assumptions about the way inheritance is done. These are checked at runtime when CVC4_ASSERTIONS is on. See src/theory/theory.h's TheoryImpl<> definition for details. * src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h, src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h, src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h, src/parser/antlr_parser.h: minor code formatting fixes as per policy. * src/theory/uf/theory_uf.cpp: fix for non-debug builds. * src/util/options.h, src/util/model.h, src/util/result.h, src/expr/type.h: make CVC4_PUBLIC. * src/util/decision_engine.h: no longer CVC4_PUBLIC. * src/expr/expr_manager.cpp: ExprManager::booleanType() and ExprManager::kindType() weren't returning a value ?! Fixed. * src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no longer depends on NodeManager (public/private interface mixing). ExprManagerScope is an internal implementation detail, and is moved to node_manager.h. * src/expr/node.h: mark gdb debug routines as "used" so that GCC always emits code for them (even though its static analysis shows they're unused).
2010-02-22Merging from branch branches/Liana r241Dejan Jovanović
2010-02-22Re-committing revision 232 properly:Morgan Deters
* Add virtual destructors to CnfStream, Theory, OutputChannel, and ExplainOutputChannel. Safer and stops a compiler warning. * node attributes: fix compiler warnings on 64-bit. * Node: add asserts to make sure the current NodeManager is non-NULL when it's needed. This can happen when public-facing functions don't properly set the node manager, and it can look like a bug in another part of the library. Also some code format cleanup. * configure.ac, config/cvc4.m4: added --enable-static-binary (see discussion on bug 33), fixed bad configure lines (bug 19), added documentation for some things. * config.h.in: removed; it's auto-generated.
2010-02-22undoing improperly-committed revision 232; will re-commit to get "svn blame" ↵Morgan Deters
correct, etc..
2010-02-22* Add virtual destructors to CnfStream, Theory, OutputChannel, andCesare Tinelli
ExplainOutputChannel. Safer and stops a compiler warning. * node attributes: fix compiler warnings on 64-bit. * Node: add asserts to make sure the current NodeManager is non-NULL when it's needed. This can happen when public-facing functions don't properly set the node manager, and it can look like a bug in another part of the library. Also some code format cleanup. * configure.ac, config/cvc4.m4: added --enable-static-binary (see discussion on bug 32), fixed bad configure lines (bug 19), added documentation for some things. * config.h.in: removed; it's auto-generated.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback