| Age | Commit message (Collapse) | Author |
|---|
|
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
|
|
|
|
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
|
|
* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.)
* Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
|
|
|
|
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!
|
|
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.
|
|
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.
|
|
|
|
1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.
No performance impact is expected outside of datatypes. I'm verifying that that is the case with a cluster job this morning.
|
|
|
|
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).
|
|
|
|
|
|
|
|
* add Stats black-box unit test
* new make target: "make units" now runs unit tests only
* revised make target: "make regress" now runs regressions only
* configure.ac: pull in librt for clock_gettime()
|
|
CongruenceClosure implementation; CongruenceClosure white-box test.
New UF theory implementation based on new CC module. This one
supports predicates. The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").
Added type infrastructure for TUPLE.
Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).
Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)
Other minor changes.
|
|
with that of Node.
* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
related to children now throw an IllegalArgumentException:
* getNumChildren()
* begin()
* end()
* operator[]
* getChild()
This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
the children are "reinterpreted" -- the first being an operator. Interface-wise,
it doesn't make sense to return one thing for nb[0], then later, after setting
the kind, to return another thing for nb[0].
* Fixed unit tests depending on this behavior.
* Added a warning to the testing summary if unit tests didn't run (because this
is likely due to compilation problems, and without a warning it looks kind of
like a test success)
* VERBOSE wasn't exported to the environment for unit test "make check." Fixed.
|
|
|
|
* keeps test logs around
* provides parallel testing functionality (with make -jN).
I've also added new functionality in test/Makefile.am which deletes old test logs, ensures that ALL tests are tried (even if units fail), and provides a color-coded summary at the end of the test run, which shows how many units, regressions (per level), and system tests failed (or passed), and provides a link to the log file for further information.
Resolves bug 117.
|
|
|
|
|
|
also support synonyms for "make check" globally
|
|
|
|
|
|
|
