summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2012-02-21language bindings fixes for yesterday's portfolio mergeMorgan Deters
2012-02-21Fix for bug303. The problem was with function applications that get ↵Dejan Jovanović
normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced. Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
2012-02-21don't require libboost_thread (its presence is detected at configure-time), ↵Morgan Deters
and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
2012-02-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in ↵Morgan Deters
my previous checkin)
2012-02-20fix "make dist"Morgan Deters
2012-02-20portfolio mergeMorgan Deters
2012-02-20Added Theory::postsolve() infrastructure as Clark requested.Morgan Deters
(Though currently unused.) For theories that request presolve and postsolve (in their kinds file), they will get a presolve() notification before the first check(). After the final check during the current search, they get a postsolve(). presolve() and postsolve() notifications always come in pairs, bracketing all check()/propagate()/getValue() calls related to a single query. In the case of incremental benchmarks, theories may get additional presolve()/postsolve() pairs, but again, they always come in pairs. Expected performance impact: none (for theories that don't use it) http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
2012-02-20By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1Morgan Deters
and SMT-LIBv2). There are --enable-symmetry-breaker and --disable-symmetry-breaker options that are always respected regardless of this default. Expected performance impact: positive New default (UF only) compared to old default (always on): http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5 Symmetry breaker remains a big win on UF: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5 The last link to results looks at first that the symmetry breaker should always be turned off, since its use loses more regressions than it gains. *However*, the lost ones are only our "QF_SAT" benchmarks. For these, we should indeed turn off the symmetry breaker, but that's impossible for now because we tag them internally with the logic "QF_UF."
2012-02-16Last commit accidentally lacked r2778 and r2779 from integer2. I have ↵Tim King
manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from ↵Tim King
r2650 to r2779. - This excludes revision 2777. This revision had some strange performance implications and was delaying the merge. - This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts. - The DioSolver can be disabled at command line using --disable-dio-solver. - This includes a number of changes to the arithmetic normal form. - The Integer class features a number of new number theoretic function. - This commit includes a few rather loud warning. I will do my best to take care of them today.
2012-02-13precision in theoryskelFrançois Bobot
2012-02-13proper handling of improper get-valueMorgan Deters
2012-02-12copyright year updated to 2012Morgan Deters
2012-02-10correct comment typo found during today's architectural meetingMorgan Deters
2012-02-09fixing antoher small bug in backtrackingDejan Jovanović
2012-02-08fixing a bug in uf_engine application lookup backtrackingDejan Jovanović
this should also fix bug299
2012-02-08Number of changes to cvc_printer.cpp. Specialized the printing for BVPLUS, ↵Tim King
BVSUB, and BVMULT. Fixed a bug in printing on PREFIX operators. Added parenthsis for POSTFIX operators. Passing the ouroborous test now.
2012-02-07fixing some missing stuffDejan Jovanović
2012-02-05changes to the cvc4 language printer, so that it actually prints the cvc4 ↵Dejan Jovanović
language all theory writers should take a look a what's being printed, to ensure all cases are covered
2012-02-04support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now ↵Andrew Reynolds
assumes uninterpretted sorts are well-founded, allowing datatypes to work with uninterpretted sort subdata
2012-02-03updating configure to use python-config for building python bindingsDejan Jovanović
2012-01-27effecting the same change in the compat Java binding as was done to CVC3 ↵Morgan Deters
yesterday (ValidityChecker::value() and ValidityChecker::getValue())
2012-01-23Partial fix to TheoryEngine::getExplanation so that SharedAssertions request ↵Tim King
explanations from the theory that can explain them. This partially fixes bug 295.
2012-01-23fix for bug295Dejan Jovanović
2012-01-17updates to smt2 parser to support datatypes, minor updates to datatypes ↵Andrew Reynolds
theory/rewriter to support datatypes with non-datatype subdata
2011-12-15Partial fix to bug 295.Tim King
2011-12-15Fix to the previous commit.Tim King
2011-12-15Partial fix in arithmetic for propagating shared terms. This partially ↵Tim King
resolves bug 289. Adds failing tests to regress1.
2011-12-14added minor documentation for parametric datatypes, for bug 283Andrew Reynolds
2011-12-14minor fixes to printing and parsing of CVC-language defined functions and ↵Morgan Deters
lambdas; resolves bug 294
2011-12-14some more bug fixes (TNode -> Node, normalize literals in explanations)Dejan Jovanović
2011-12-12* merging some uf stuff from incremental_work branch that somehow nobody ↵Dejan Jovanović
merged-in * since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet
2011-12-10adding additional checks for theories propagating literals that already have ↵Dejan Jovanović
a value
2011-12-10a bit more changes, when propagting equalities/dis-equalities don't assert ↵Dejan Jovanović
them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.
2011-12-10attempt to fix bug 293: if a split on a trivial shared pair is requested ↵Dejan Jovanović
from a theory, such as 1 = 0, it is reasserted to the theory.
2011-12-08Disable a BV rewriter statistic (after checking with Liana) that was static,Morgan Deters
and thus caused big problems with programs that create two SmtEngines in one process. If we need state like this in the rewriters, we'll need to make them nonstatic.
2011-12-06LemmaStatus changes, as agreed to during 12/2 meeting.Morgan Deters
2011-12-06oops, removing some integer operations that leaked in (they aren't part of ↵Morgan Deters
trunk yet)
2011-12-06fix errors in smt-lib2 output; needed for debuggingMorgan Deters
2011-12-05change short-circuiting behavior of Command execution in the main driver; ↵Morgan Deters
allows a (limited) form of error recovery, matching what we had previously
2011-12-02Error detection is different now---with new Command infrastructure, ↵Morgan Deters
exceptions are not thrown outside the library. Reflect this in the exit code of the driver. Fixes a bug found by Tim among the nightly regressions. Also improved error reporting if antlr is unavailable and the parsers need to be generated.
2011-11-30fix linking errors on oneiricMorgan Deters
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic ↵Tim King
now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
2011-11-26Fix Java JNI installation pathMorgan Deters
2011-11-22fix module name for CVC4 jar file; part of the fix for the Debian package ↵Morgan Deters
build failure last night
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-16Fix "make dist". Fixes to python and ruby bindings; ruby example written. ↵Morgan Deters
They should both work out of the box, now, with swig 2.0.4 at least. "make install" likely still needs to be adjusted to install them sensibly.
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-16fix to build system for java bindingsMorgan Deters
2011-11-16* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!Morgan Deters
* Also some better configure script wording
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback