Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-02-03 | Some cleanup of miplib regressions and options | Morgan Deters | |
2013-02-03 | Merge from mdeters/miplib branch (commit ↵ | Morgan Deters | |
'ce7c485182902ae43871057185095f71f74a8a58') | |||
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters | |
2013-02-01 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-01 | Fix a tuple attribute bug that was causing model-generation problems for tuples | Morgan Deters | |
2013-01-29 | currently disabling bug486 regression. we need to discuss ↵ | Andrew Reynolds | |
getValue/collectModelInfo for quantifiers more. | |||
2013-01-28 | Fix the regression test for bug 486, and enable it | Morgan Deters | |
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87) | |||
2013-01-28 | Fix the regression test for bug 486, and enable it | Morgan Deters | |
2013-01-28 | some fixes for win32, including ability to "make check" win32 builds via wine | Morgan Deters | |
2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters | |
2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters | |
2013-01-08 | SMT-LIB get-model output now is easier to machine-parse: contains (model...) ↵ | Morgan Deters | |
bracketing | |||
2012-12-11 | SMT-LIB compliance fix to get-assignment; resolves bug 480 | Morgan Deters | |
2012-12-06 | Fix for fuzzer-found model bug | Clark Barrett | |
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79) | |||
2012-12-01 | remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵ | Morgan Deters | |
failing regression for bug 472 | |||
2012-12-01 | Some fixes for boolean arrays | Morgan Deters | |
also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-30 | Add some regressions for bug 438. | Morgan Deters | |
(this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-30 | fix rewrite-rules syntax in regression | Morgan Deters | |
2012-11-30 | fix the syntax of assert-rewrite/-propagation/-reduction by putting the ↵ | François Bobot | |
pattern first just after the bindings Do it before the release in order to not break user files later | |||
2012-11-29 | reliable benchmark corresponding to bug468 | Kshitij Bansal | |
2012-11-27 | Functions and predicates over Boolean now work with --check-models and ↵ | Morgan Deters | |
output correct models for such functions (though they are somewhat ugly at present). There's still a problem with model extraction, but it's not Boolean terms' fault. Sometimes checkModel() can report that the model is just fine, but if a user extracts values with getValue(), they find problems with the model (i.e., it doesn't satisfy some assertions). This appears to be due to an asymmetry between how checkModel() works and how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking some more on it. (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-27 | First chunk of boolean-terms support. | Morgan Deters | |
Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-27 | Tuples and records merge. Resolves bug 270. | Morgan Deters | |
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-26 | fixup for incremental solving | Dejan Jovanović | |
2012-11-26 | Removing DioSolver::acceptableOriginalNodes(). This assertion was too ↵ | Tim King | |
strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case. | |||
2012-11-26 | Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run ↵ | Tim King | |
in debug mode. This is too long for a regress0 test. | |||
2012-11-25 | Adding a regression test from bug 462. | Tim King | |
2012-11-23 | Example of rewrite rules use that comes from an harness test | François Bobot | |
2012-11-19 | Adding hand minimized test for bug 450. | Tim King | |
2012-11-17 | Fixed last currently known bug in array models | Clark Barrett | |
2012-11-17 | * enable previously-failing (now succeeding) datatype example that uses records | Morgan Deters | |
* some bindings cleanup (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-16 | Fix for bug451 | Clark Barrett | |
2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett | |
Also refactored some header file includes to reduce compile time | |||
2012-11-15 | fuzz15 should have been fuzz14 | Clark Barrett | |
2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett | |
similar to arrays - limit the set of terms reported to those relevant in the current context. Also removed collectModelInfo from sharedTermsDatabase - doesn't seem to be needed any more. | |||
2012-11-15 | Fixing comments in print_lambda.cvc. | Tim King | |
2012-11-14 | Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ↵ | Tim King | |
printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language. | |||
2012-11-14 | Fix to bug449. Adds shared constants to the set of DeltaRationals that must ↵ | Tim King | |
be in the final total order. | |||
2012-11-14 | bug fixes to models, array rewriter with previously failing testcases | Clark Barrett | |
2012-11-13 | added support for division by zero for bit-vector division operators | Liana Hadarean | |
2012-11-13 | Fixed an array rewriting bug found by fuzzer | Clark Barrett | |
2012-11-13 | Testcases for fixed bugs | Clark Barrett | |
2012-11-12 | Improved error reporting for improperly using non-linear division in linear ↵ | Tim King | |
arithmetic. | |||
2012-11-12 | Delta is now generated in arithmetic to keep consistent the total order of ↵ | Tim King | |
DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees. | |||
2012-11-10 | Fixed missing \ in uflra/Makefile.ma | Clark Barrett | |
Fixed another model bug and added previously failing fuzz testcase | |||
2012-11-10 | Fix for bug 439. Delta computation now includes disequality information. | Tim King | |
2012-11-10 | Change run-regression script to *additionally* run a second test with ↵ | Morgan Deters | |
--check-models *if* the benchmark is sat/invalid (or is incremental, with at least one sat/invalid result). This increases significantly the time to do a "make regress", as more tests are running. We need to run both *with* and *without* --check-models, since that option disables certain preprocessing. To turn off these extra tests during a make regress, you can set CVC4_REGRESSION_ARGS=--no-check-models. To turn off the extra test for a *particular* regression benchmark, you can put this in the benchmark: ; COMMAND-LINE: --no-check-models That might be necessary in e.g. nonlinear arithmetic benchmarks. (this commit was certified error- and warning-free by the test-and-commit script.) | |||
2012-11-09 | Test that breaks arithmetic model building due to disequality terms. | Tim King | |
2012-11-09 | Arithmetic problem that fails --check-models due incompleteness with ↵ | Tim King | |
multiplication. | |||
2012-11-08 | Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases ↵ | Tim King | |
for division by 0. |