| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
regressions.
|
|
|
|
of term database, other refactoring. Bug fixes for cbqi+datatypes.
|
|
report. Other minor cleanup.
|
|
bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
|
|
Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
|
|
|
|
tff script. Minor additions to sygus.
|
|
signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
|
|
Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.
Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.
QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master.
Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.
Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE.
Merging rewrite rules into master, check-model current fails on 3 FMF regressions.
Fix check-model issue, a line of code was omitted during merge.
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
success, nonzero error
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
in debug mode. This is too long for a regress0 test.
|
|
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
|
|
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_01.smt2
z3: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat unsat
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_02.smt2
z3: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat unsat
|
|
* Ensure Rewriter::init() is called before ::rewrite().
The array type enumerator recently gave us an end-run around
::init(). TheoryEngine no longer calls these, they're done
via static initialization.
* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* ITE removal fixed to be context-dependent (on UserContext).
Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
(partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
was labeled sat); re-enable it for "make regress"
Also:
* --check-model doesn't fail if quantified assertions don't simplify away.
* fix some examples, and the Java system test, for the disappearance of the
BoolExpr class
* add copy constructor to array type enumerator (the type enumerator
framework requires copy ctors, and the automatically-generated copy ctor
was copying pointers that were then deleted, leaving dangling pointers in
the copy and causing segfaults)
* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
you to dump before/after a particular preprocessing pass. E.g.,
--dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
"--dump=assertions" by itself is after all preprocessing, just before CNF
conversion.
* minor fixes to dumping output
* include Model in language bindings
Minor refactoring/misc:
* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
(e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications
|
|
regress, because the bug was fixed.
Also make QuantifiersModule's destructor virtual (it has virtual members).
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
should work now
|
|
recently-fixed incremental bugs are closed
|
|
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
|
|
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
|
|
but a push/pop or multiple query is attempted (previously it could give
incorrect answers)
Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).
Also fix mkbuilddir script for when it's called from contrib/switch-config.
|
|
|
|
|
|
|
