summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Collapse)Author
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-23Added ability to set a "cvc4-specific logic" in standards-compliantMorgan Deters
SMT-LIBv1 and SMT-LIBv2 input: In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance: (benchmark actually_a_sat_benchmark_but_looks_like_uf :logic QF_UF :cvc4_logic { QF_SAT } [...] In SMT-LIBv2, you use a set-info; for instance: (set-logic QF_UF) (set-info :cvc4-logic "QF_SAT") [...] Right now, the only thing this does is disable the symmetry breaker for benchmarks like the above ones. As part of this work, TheoryEngine::setLogic() was removed (the logic field there wasn't actually used anywhere, its need disappeared when Theory::setUninterpretedSortOwner() was provided). Also, Theory::d_uninterpretedSortOwner got a name change to Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory class. This represents a breakage of our separation goals for CVC4, since it means that two SmtEngines cannot be created separately to solve a QF_AX and QF_UF problem. A bug report is pending.
2012-02-22Fixes to documentation / fixes for MacOSMorgan Deters
2012-02-21fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on ↵Morgan Deters
platforms that need it; fixes Mac builds.
2012-02-21language bindings fixes for yesterday's portfolio mergeMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2012-02-13proper handling of improper get-valueMorgan Deters
2011-12-14minor fixes to printing and parsing of CVC-language defined functions and ↵Morgan Deters
lambdas; resolves bug 294
2011-11-22More language bindings work:Morgan Deters
* with a patched SWIG, the ocaml bindings build correctly. ** I will provide my patch to the SWIG dev team. * fixed some class interfaces to play more nicely with SWIG. * php, perl, tcl now work; examples added. * improved binding module building and installation. Also: Stop #defining NULL ((void*) 0). This has been in cvc4_public.h for a long, long time, I forget why I added it in the first place, and it's a very, very bad idea. In C++, certain things are permitted for NULL that aren't permitted for ((void*) 0), like for instance implicit conversion to any pointer type. We didn't see an issue here (until now, when interfacing with SWIG), because GCC is usually pretty smart at working around such a broken #definition of NULL. But that's fragile. New exception-free Command architecture. Previously, some command invocations were wrapped in a try {} catch() {} and printed out an error. This is much more consistent now. Each Command invocation results in a CommandStatus. The status can be "unsupported", "error", or "success" (these are each derived classes, though, not strings, so that they can be easily printed in a language-specific way... e.g., in SMT-LIBv2, they are printed in a manner consistent with the spec, and "success" is not printed if the print-success option is off.) All Command functionality are now no-throw functions, which @cconway reports is a Good Thing for Google (where all C++ exceptions are suspect), and also I think is much cleaner than the old way in this instance. Added an --smtlib2 option that enables an "SMT-LIBv2 compliance mode"---really it just sets a few other options like strictParsing, inputLanguage, and printSuccess. In the future we might put other options into a compliance mode, or we might choose to make it the default.
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ↵Morgan Deters
Datatypes (bug #283) by Chris Conway. Thanks, Chris!
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-06datatype stuff in compatibility interface implementedMorgan Deters
2011-11-04STRING_TYPE and CONST_STRING and associate type infrastructure implemented.Morgan Deters
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-29fix unit testsMorgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵Morgan Deters
SmtEngine::getProof(), a few other things..
2011-10-28* ability to output NodeBuilders without first converting them to ↵Morgan Deters
Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup
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-10-07Some new Datatype public functionality, as per Chris Conway's suggestions on ↵Morgan Deters
the dev mailing list.
2011-10-05Reverting a fix from earlier today that fixed a Mac OS warning but ↵Morgan Deters
completely broke Linux. :-(
2011-10-05minor visibility fixesMorgan Deters
2011-10-04Yet Another Antlr3 Mod---this time, all my fault: for configuration ↵Morgan Deters
auto-detection of libantlr3c, I chose an innocent-looking function that was present in both versions. But it's signature had changed, breaking source compatibility in both directions. Just like the other function that started the whole mess. Silly me.
2011-09-30interfaces fixes and cleanups...and examples of each interface!Morgan Deters
2011-09-29build system fixesMorgan Deters
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-23interface cleanup, java bindings workMorgan Deters
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-20Merge from "swig" branch: language binding for Java is compiling and ↵Morgan Deters
linking. Enable with --enable-language-bindings=java
2011-09-16dump define-funs correctly with "--dump declarations", whether the function ↵Morgan Deters
is defined via API or through input language
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
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-07-11merge from symmetry branchMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's ↵Morgan Deters
more than one "real" theory (not BUILTIN or BOOL) active
2011-06-30some things I had laying around in a directory but never got committed; ↵Morgan Deters
minor fix-ups to documentation and some node stuff
2011-06-18Some fixes inspired by Fedora 15:Morgan Deters
* compilation fixes for GCC 4.6.x + ptrdiff_t is now in std:: * fix some make rules that are ok in Make 3.81 but broke in Make 3.82 * look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include
2011-06-06Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, ↵Morgan Deters
on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address. Resolves bug #263. Also, some debugging improvements.
2011-06-03datatypes workMorgan Deters
2011-06-01minor fix, and better output for type errorsMorgan Deters
2011-06-01type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]Morgan Deters
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-14reverting node manager change from 1881; also part of parameterized ↵Morgan Deters
datatypes review
2011-05-14add AscriptionType stuff to support nullary parameterized datatypes; also, ↵Morgan Deters
review of Andy's earlier commit, with some minor code clean-up and documentation
2011-05-13added support for parametric datatypes, updated cvc parser to handle ↵Andrew Reynolds
parametric datatypes, type ascriptions are not implemented yet
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback