summaryrefslogtreecommitdiff
path: root/src/prop/cnf_stream.h
AgeCommit message (Collapse)Author
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-07Update copyright headers.Mathias Preiner
2016-11-07Fixing a memory leak in the CnfStream unit tests.Tim King
2016-07-24Proper handling for lemmas that are conjuncts:Guy
Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked. Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
2016-01-28Adding listeners to Options.Tim King
- Options -- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options. -- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners. -- Added functions to Options for registering listeners of the notify calls. -- Changed a number of options to use the new listener infrastructure. -- Fixed a number of warnings in options. -- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure. -- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}. - Theories -- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options. - Ostream Handling: -- Added new functionality that generalized how ostreams are opened, options/open_stream.h. -- Simplified the memory management for different ostreams, smt/managed_ostreams.h. -- Had the SmtEnginePrivate manage the memory for the ostreams set by options. -- Simplified how the setting of ostreams are updated, smt/update_ostream.h. - Configuration and Tags: -- Configuration can now be used during predicates and handlers for options. -- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/. -- Moved {Debug,Trace}_tags.* from being generated in options/ into base/. - cvc4_private.h -- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's. -- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations. -- Made lib/lib/clock_gettime.h a cvc4_private_library.h header. - Antlr -- Fixed antlr and cvc4 macro definition conflicts that caused warnings. - SmtGlobals -- Refactored replayStream and replayLog out of SmtGlobals. -- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-05Add SmtGlobals ClassTim King
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library. - The option replayLog has been removed due to inconsistent memory management. - SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently. - There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine. - A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction. - Selected classes have been given a copy of this pointer in their constructors. - Removed the dependence on Node from Result. Moving Result back into util/.
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ajreynol
signature. Add regressions.
2014-11-17Resource-limiting work.Liana Hadarean
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback