summaryrefslogtreecommitdiff
path: root/src/theory/output_channel.h
AgeCommit message (Collapse)Author
2014-07-01Update copyrights.Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas ↵Morgan Deters
(resolves bug #548).
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-05-02* splitLemma to request atomsDejan Jovanović
* normalizing in bv before bitblasting
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Adding demand restart.Tim King
2013-04-01Merging some cleanup work:Morgan Deters
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
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-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to ↵Morgan Deters
make it unambiguous for case-insensitive filesystems like on Mac. Fixes Mac builds
2012-08-31merge from fmf-devel branch. more updates to models: now with ↵Andrew Reynolds
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-08-16Replace propagateAsDecision() with Theory::getNextDecisionRequest():Morgan Deters
* arrays now uses the new approach by using a CDQueue<> * uf strong solver has had the feature disabled, pending a merge from Andy * theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property) * the staticLearning property has been renamed ppStaticLearn to match the function name * theory kinds files are now checked again for correctly-declared properties (this had been disabled) * minor documentation and other fixups
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-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-02-22Added OutputChannel::propagateAsDecision() functionality, allowing a theoryMorgan Deters
to request a decision on a literal. All these theory requests are kept in a context-dependent queue and serviced in order when the SAT solver goes to make a decision. Requests that don't have a SAT literal give an assert-fail. Requests for literals that already have an assignment are silently ignored. Since the queue is CD, requests can actually be serviced more than once (e.g., if a request is made at DL 5, but not serviced until DL 10, and later, a conflict backtracks to level 7, the request may be serviced again). Performance impact: none to negligible for theories that don't use it See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0
2011-12-06LemmaStatus changes, as agreed to during 12/2 meeting.Morgan Deters
2011-10-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want). * Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch. * --limit / --time-limit options renamed --rlimit and --tlimit. There may be slowdown from disabling pseudobooleans.
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-15additional stuff for sharing, Dejan Jovanović
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-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-08-27Removing Theory::registerTerm() as discussed in the meeting. Now ↵Dejan Jovanović
pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).
2011-04-14Three things:Morgan Deters
1. Infrastructure for unit T-conflicts added to SAT proxy (and also the theory output channel documentation); previously theories could not communicate unit T-conflicts with the SAT layer because that layer had an implicit assumption (not asserted) that the conflict nodes were an AND. 2. UF now pre-rewrites trivial equalities to "true". These could conceivably occur in artificial benchmarks in this form: (let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... ) 3. The SMT-LIBv2 printer now properly prints Bool constants.
2011-04-04Add documentation to Node and TNode (closes bug #201).Morgan Deters
Also, only build doxygen documentation on stuff in src/, not test/ or contrib/ or anywhere else. Hopefully this turns our 3000+ page user manual into something a little more useful!
2010-11-19Merge from ufprop branch, including:Morgan Deters
* Theory::staticLearning() for statically adding new T-stuff before normal preprocessing. UF's staticLearning() does transitivity of equality/iff, solving the diamonds. * more aggressive T-propagation for UF * new KEEP_STATISTIC macro to hide Theories from having to register/deregister statistics (and also has the advantage of keeping the statistic type, field name, and the 'tag' used to output the statistic in the same place---instead of scattered in the theory definition and constructor initializer list. See documentation for KEEP_STATISTIC in src/util/stats.h for more of an explanation). * more statistics for UF * restart notifications from SAT (through TheoryEngine) via Theory::notifyRestart() * StackingMap and UnionFind unit tests * build fixes/adjustments * code cleanup; minor other improvements
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-10-24add a CVC4_UNDEFINED keyword, for intentionally undefined functions (like ↵Morgan Deters
private copy constructors and assignment, for instance) that generates better, compile-time error messages if the function is used (before, you'd have to wait until link time); also some minor cleanup
2010-10-12hooked up "we are incomplete" flag after conversation with Tim (a theory ↵Morgan Deters
notifies the theory engine through its output channel); some cleanup; add a regression for bug #216
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, ↵Morgan Deters
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
2010-10-03file header documentation regenerated with contributors names; no code ↵Morgan Deters
modified in this commit
2010-07-06Moved registration to theory engineClark Barrett
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-05-27Preregistration has been turned on. Highly experimental eager splitting ↵Tim King
support has been added. Also a few bug fixes to Tableau.
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-25* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.Morgan Deters
There remain memory leaks (and some over-decrementing of refcounts) that I've identified; another commit forthcoming. * src/expr/attribute.h: keys are now NodeValue* instead of TNode * src/theory/output_channel.h: change OutputChannel::conflict() to the negation of what we had before: it now takes an AND of TRUE literals as a conflict clause rather than an OR of FALSE ones. * src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine for use inside gdb * src/expr/node.h: remove Node::debugPrint() member (now a function instead of a member function, since Node is now a template it wasn't being properly instantiated(?) and couldn't be called from gdb) * src/expr/Makefile.am: add node.cpp * src/expr/node_manager.h: code formatting
2010-02-25* src/expr/node.h: add a copy constructor. Apparently GCC doesn'tMorgan Deters
recognize an instantiation of the join conversion/copy ctor with ref_count = ref_count_1 as a copy constructor. Problems with reference counts ensue. * src/theory/theory.h, src/theory/theory.cpp: Theory base implementation work. Changed from continuation-style theory calls to having an data member for the output channel. registerTerm() and preRegisterTerm() work. * src/theory/output_channel.h, src/theory/theory.h, src/theory/theory.cpp, src/theory/uf/theory_uf.h, src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into OutputChannel. * test/unit/expr/node_black.h: remove testPlusNode(), testUMinusNode(), testMultNode(). * src/expr/attribute.h: new facilities ManagedAttribute<> and CDAttribute<>, and add new template parameters to Attribute<>. Make CDAttribute<>s work with context manager. * src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and TypeAttr are now "owned" (defined) by the NodeManager. The AttributeManager knows nothing of specific attributes, it just as all the code for dealing generically with attributes. * test/unit/expr/node_white.h: test new attribute facilities. * src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes away. * src/theory/Makefile.am: fixed improper linking of theories * src/theory/theory_engine.h: some implementation work (mainly stubs for now, just to make sure TheoryUF can be instantiated properly, etc.) * src/expr/node_value.cpp, src/expr/node_value.h: move a number of function implementations to the header and make them inline * src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of function implementations to the header and make them inline * src/theory/theoryof_table_prologue.h, src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof, src/theory/Makefile.am: make the theoryOf() table from kinds and implement TheoryEngine::theoryOf(). * src/theory/arith/Makefile, src/theory/bool/Makefile: generated these stub Makefiles (with contrib/addsourcedir) as per policy * src/theory/arith, src/theory/bool [directory properties]: add .deps to svn:ignore. * contrib/configure-in-place: permit configuring "in-place" in the source directory. * contrib/get-authors, contrib/dimacs_to_smt.pl, contrib/update-copyright.pl, contrib/get-authors, contrib/addsourcedir, src/expr/mkkind: copyright notice * src/expr/node_manager.h, src/expr/node_builder.h, src/prop/prop_engine.h, src/prop/prop_engine.cpp, src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp, src/theory/output_channel.h: turn "const Node&"-typed formal parameters into "TNode" * src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans" to avoid keyword clash on containing namespace * src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h, src/theory/arith/theory_def.h: "define" a theory simply (for automatic theoryOf() generator). * src/Makefile.am: build theory subdirectory before prop, smt, etc. so that src/theory/theoryof_table.h header gets generated before it's needed * src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a separate CVC4::kind namespace to avoid its contents from cluttering the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace but not the enum values. * src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h, src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp, src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g, src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp, test/unit/expr/node_white.h, test/unit/expr/node_black.h, test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h: update for having moved Kind into CVC4::kind. * src/parser/parser.cpp: added file-does-not-exist check (was failing silently).
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.
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides ↵Morgan Deters
cvc4-c++-editing-mode from contrib/editing-with-emacs
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; ↵Morgan Deters
regenerated configure script
2010-02-04Added theory output channel interfaces and "Interrupted" exception.Morgan Deters
Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs. Updated copyright year. Added a new "bool" theory (right now just to hold a kind.h contribution). Added "kinds" files to UF and the new "bool" theory.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback