summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Collapse)Author
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-28merged the proofgen3 branch into trunk:Liana Hadarean
- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
2011-10-25Initialize resource limit and millisecond limit optionsKshitij Bansal
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-21add gcc version information to Configuration, and warn when building with ↵Morgan Deters
v4.5.1 which has a buggy optimizer (resolves bug #266)
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-10-07Some new Datatype public functionality, as per Chris Conway's suggestions on ↵Morgan Deters
the dev mailing list.
2011-10-05minor visibility fixesMorgan Deters
2011-10-05remove some debugging code that slowed down last night's regressionsMorgan Deters
2011-10-04Disabling the variable removal hueristic by default.Tim King
2011-10-04cvc3 compatibility layer; and another libantlr3c v3.4 incompatibility fixMorgan Deters
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30interfaces fixes and cleanups...and examples of each interface!Morgan Deters
2011-09-29compatibility work, documentationMorgan Deters
2011-09-29build system fixesMorgan Deters
2011-09-29some test fixesMorgan Deters
2011-09-28variety of visibility fixes (should clean up some of the many warnings on ↵Morgan Deters
MacOS-production-dynamic builds)
2011-09-28CVC4::Integer was not marked CVC4_PUBLIC, causing dynamic link errors on ↵Morgan Deters
MacOS in production builds. Fixed.
2011-09-28fixes for make dist ; make installMorgan Deters
2011-09-28better fix for #281, also fix issue with command line options not existing ↵Morgan Deters
on older g++en, like Apple's 4.2 on Snow Leopard.
2011-09-28Regular expressions in shell scripts on MacOS are inconsistent... again. :-( ↵Morgan Deters
Fixing a problem with Debug_tags and Trace_tags, closes bug #281
2011-09-28removed "typename" keyword (fix to bug 280)Morgan Deters
2011-09-23interface cleanup, java bindings workMorgan Deters
2011-09-21Java binding now working. Some interface types still need some work (e.g. ↵Morgan Deters
iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
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-17--show-debug-tags and --show-trace-tags now supported by Configuration API; ↵Morgan Deters
also, the information is only recompiled and relinked when it has changed, avoiding unnecessary relinking
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-15adding --show-debug-tags to list all available debug tracing tagsDejan Jovanović
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-08-24Simplification of the preregister and register throught a NodeVisitor class. ↵Dejan Jovanović
The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11merge from symmetry branchMorgan Deters
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to ↵Tim King
16. Enabled arithmetic propagation and variable removal by default. Changed the command line arguments for both propagation and variable removal allow for disabling these.
2011-06-30Merging the playground branch upto r1957 into trunk.Tim King
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-29Fixed spelling mistake and documentation for --enable-variable-removal.Tim King
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-03fixed various bugs related to ambiguous parametric datatype constructors, ↵Andrew Reynolds
parametric datatype versions of paper benchmarks are now working
2011-06-03datatypes workMorgan Deters
2011-06-02added (temporary) support for ensuring that all ambiguously typed ↵Andrew Reynolds
constructor nodes created internally are given a type ascription
2011-06-01type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]Morgan Deters
2011-05-31This commit contains the code for allowing arbitrary equalities in the ↵Tim King
theory of arithmetic. * This code has been partially tested. (My testing situation is currently not so great.) The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures. This does pass make regress as well as a fresh checkout does. (The Mac version has issues.) * I need to disable the permanent row removal heuristic by default. We need to discuss why this needs to happen. We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done. * I have disabled the arithmetic rewrite equality flag. This code needs to be added to the parser. * For all of the above changes, I have annotated the code with the key word BREADCRUMB. * I have renamed ArithUnatePropagator to ArithAtomDatabase.
2011-05-28include subversion information used for each build in the --show-config ↵Morgan Deters
output and as a banner in --interactive mode; intended to resolve confusion in cases where you don't know where a CVC4 binary came from
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback