summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-27more interface work; adding legacy C interfaceMorgan Deters
2011-09-25first crack at compatibility java interface (not built by default)Morgan Deters
2011-09-24Fix to building and linking for unit tests. (This should fix the ↵Morgan Deters
segfaulting units in optimized-dynamic. The problem was that the code incorrectly determined the address of one of the thread-scoped global variables, and I think it's because the same library was linked twice into the unit test in two different ways, confusing the runtime support code.)
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-20fix 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-16dump define-funs correctly with "--dump declarations", whether the function ↵Morgan Deters
is defined via API or through input language
2011-09-16include example theory (former "UF-Tim") that's included in the dist but not ↵Morgan Deters
built for the library
2011-09-16final(?) documentation fixesMorgan Deters
2011-09-16fix up more documentationMorgan Deters
2011-09-16some minor fixes to the cvc3 compatibility library and test caseMorgan Deters
2011-09-16fix serious issue with copyright-updating scriptMorgan Deters
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-16fix an oversight in the language printersMorgan Deters
2011-09-15tim's fixes for context-dependent pre-registrationDejan Jovanović
2011-09-15adding --show-debug-tags to list all available debug tracing tagsDejan Jovanović
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-07fixes for uf/equality engine from the quantifiers branch. mainly ↵Dejan Jovanović
backtracking issues.
2011-09-03Disable a warning to address bug 277. (This doesn't really resolve the ↵Morgan Deters
issue, but the warning isn't dangerous here. See the bugzilla comments.)
2011-09-03removing an assert i forgot to remove that andy foundDejan 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-02Ensure that assignment gestures through CDMap iterators like:Morgan Deters
(*myCDMap.find(foo)).second = bar; fail with a compile-time error (rather than being silently ignored, like they had been). Resolves bug #276.
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-09-02* Changing pre-registration to be context dependent -- it is called from the ↵Dejan Jovanović
SAT solver on every backtrack * Updated UF to handle the context dependent pre-registration * Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool
2011-08-30Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK ↵Dejan Jovanović
will be reissued. Some unexpected slowdowns, but not too much.
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-08-23some uf cleanupDejan Jovanović
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-12fix bug 272, array unsoundness, and some array cleanupMorgan Deters
2011-07-11fixing out of place typename (error on g++ 4.4.3-4ubuntu5)Morgan Deters
2011-07-11Adding static_fact_managerClark Barrett
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11fix some confusing debug output (bogus counter)Morgan Deters
2011-07-11if running in QF_AX, equalities over terms of uninterpreted sort go to ↵Morgan Deters
arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
2011-07-11adding disequality propagationDejan Jovanović
relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5
2011-07-11merge from symmetry branchMorgan Deters
2011-07-10Reverting mistaken check-inClark Barrett
2011-07-10changing the sat solver remove clauses constantsDejan Jovanović
with these we get closer to yices on uf and it seems better on lra vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471 vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576
2011-07-10Fixed bug in default solve - wasn't returning when it was supposed toClark Barrett
2011-07-10another typoDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback