Age | Commit message (Collapse) | Author |
|
--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.)
|
|
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
- include directive works
- no keyword : 'fof', 'cnf', ... can be used for symbols name
- real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
- same thing for string
But:
- string not distinct by projection to real, not sure if the current state of string theory make them distinct
- filtering in include is not done
- the result is not printed in the TPTP way (currently SMT2 way)
|
|
* Fix DefineFunctionCommand when a constant is defined
|
|
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!
|
|
SmtEngine::getProof(), a few other things..
|
|
|
|
branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
(where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF
|
|
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
|
|
|
|
|
|
causing a hang in bug220.smt2
|
|
hopefully this will somewhat alleviate the problem with all the junk files in /tmp
|
|
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.
|
|
supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
|
|
|
|
enabled by mistake in the last commit
|
|
Enabled new UF theory by default.
Added some UF regressions.
Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing. (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)
Added pre-rewriting to TheoryBool which rewrites:
* (IFF true x) => x
* (IFF false x) => (NOT x)
* (IFF x true) => x
* (IFF x false) => (NOT x)
* (IFF x x) => true
* (IFF x (NOT x)) => false
* (IFF (NOT x) x) => false
* (ITE true x y) => x
* (ITE false x y) => y
* (ITE cond x x) => x
Added post-rewriting that does all of the above, plus normalize IFF and ITE:
* (IFF x y) => (IFF y x), if y < x
* (ITE (NOT cond) x y) => (ITE cond y x)
(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)
A little more debugging output from CNF stream, context pushes/pops,
ITE removal.
Some more documentation.
Fixed some typos.
|
|
|
|
post-rewrite, another full rewrite is performed and the results
compared).
Also added another response code to rewriters. Theories return a
CVC4::theory::RewriteResponse from preRewrite() and postRewrite().
This class has nice subclasses to make the theory rewriters somewhat
self-documenting in termination behavior. They look like
tail-recursive rewriting calls, but they're not; they are
instantiations of the RewriteResponse result code, which carries the
Node being returned:
// Flags the node as DONE pre- or post-rewriting, though this is
// ignored if n belongs to another theory.
//
// NOTE this just changed name from RewritingComplete(), which
// didn't match RewriteAgain().
//
return RewriteComplete(n);
// Flags the node as needing another pre-rewrite (if returned from a
// preRewrite()) or post-rewrite (if returned from a postRewrite()).
//
return RewriteAgain(n);
// Flags the node as needing another FULL rewrite. This is the same
// as RewriteAgain() if returned from preRewrite(). If it's returned
// from postRewrite(), however, this causes a full preRewrite() and
// postRewrite() of the Node and all its children (though the cache is
// still in effect, which might elide some rewriting calls).
//
// This would have been another fix for bug #168. Its use should be
// discouraged in practice, but there are places where it will
// probably be necessary, where a theory rewrites a Node into
// something in another theory about which it knows nothing.
// A common case is where the returned Node is expressed as a
// conjuction or disjunction of EQUALs, or a negation of EQUAL,
// where the EQUAL is across terms in another theory, and that EQUAL
// subterm should be seen by the owning theory.
//
return FullRewriteNeeded(n);
|
|
additional output). If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines). However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse). So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.
|
|
smt and smt2 regressions; resolves bug 132
|
|
broken, so it doesn't run with "make check")
|
|
NodeManager (bug #65). Better documentation, etc.
* As part of this, removed NodeManager::mkVar() (which created a
variable of unknown type). This requires changes to lots of unit
tests, which were using this function.
* Performed some review of parser code (my code review #73).
+ I changed the way exceptions were caught and rethrown in
src/parser/input.cpp.
+ ParserExceptions weren't being properly constructed (d_line and
d_column weren't intiialized and could contain junk, leading to
weird error messages). Fixed.
* Fix to the current working directory used by run_regression script.
Makes exceptional output easier to match against (in expected error
output).
* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
compile any C code and don't use the C++ compiler.
|
|
instead of assuming it's atomic based on kind. Atomicity is
determined at node building time. Fixes bug #81. If this is
determined to make node building too slow, we can allocate another
attribute "AtomicHasBeenComputed" to lazily compute atomicity.
* TheoryImpl<> has gone away. Theory implementations now derive from
Theory directly and share a single RegisteredAttr attribute for term
registration (which shouldn't overlap: every term is "owned" by
exactly one Theory). Fixes bug #79.
* Additional atomicity tests in ExprBlack unit test.
* More appropriate whitebox testing for attribute ID assignment
(AttributeWhite unit test).
* Better (and more correct) assertion checking in NodeBuilderBlack.
* run-regression script now checks exit status against what's provided
in "% EXIT: " gesture in .cvc input files, and stderr against
"% EXPECT-ERROR: ". These can be used to support intended failures.
Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions
in repository.
* Solved some "control reaches end of non-void function" warnings in
src/parser/bounded_token_buffer.cpp by replacing
"AlwaysAssert(false)" with "Unreachable()" (which is known
statically to never return normally).
* Regression tests now use the cvc4 binary under
builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
may not be properly installed yet at that point of the build.
(Partially fixes bug #46.)
* -fvisibility=hidden is now included by configure.ac instead of each
Makefile.am, which will make it easier to support platforms
(e.g. cygwin) that do things a different way.
* TheoryUF code formatting. (re: my code review bug #64)
* CDMap<> is leaking memory again, pending a fix for bug #85 in the
context subsystem. (To avoid serious errors, can't free context
objects.)
* add ContextWhite unit test for bug #85 (though it's currently
"defanged," awaiting the bugfix)
* Minor documentation, other cleanup.
|
|
and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.
|
|
|
|
|