| Age | Commit message (Collapse) | Author |
|---|
|
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
|
|
|
|
* 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
|
|
|
|
finite/well-founded check.
|
|
|
|
finding this)
|
|
|
|
|
|
* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.
|
|
Expected performance impact outside of datatypes/CVC parser is
negligible.
* CVC language LAMBDA, functional LET, type LET, precedence fixes,
bitvectors, and arrays, with partial parsing support also for
quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
these are complicated because they have to be left unresolved
at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
(not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
|
|
|
|
|
|
|
|
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
|
|
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.
|
|
|
|
|
|
trunk commits)
|
|
|
|
(library-internal-only of course) between Exprs and Nodes, Types and TypeNodes, ExprManagers and NodeManagers.
|
|
change the search
|
|
1. Infrastructure for unit T-conflicts added to SAT proxy
(and also the theory output channel documentation);
previously theories could not communicate unit T-conflicts
with the SAT layer because that layer had an implicit
assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true". These could
conceivably occur in artificial benchmarks in this form:
(let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.
|
|
|
|
|
|
|
|
before, leading to terrible slowdown on heavily-nested LETs (and defined functions)
|
|
|
|
|
|
|
|
|
|
|
|
newswire-raised documentation issues.
|
|
|
|
|
|
|
|
|
|
the sat solver. Also added command line options for setting both.
|
|
|
|
preregistration is now called during the conversion to cnf. This fixes bug 257.
|
|
|
|
Also, only build doxygen documentation on stuff in src/,
not test/ or contrib/ or anywhere else. Hopefully this
turns our 3000+ page user manual into something a little
more useful!
|
|
called. The OutputChannel is now untouched by TheoryArith during preregistration.
|
|
successful link at configure time
|
|
|
|
|
|
|
|
* Makes Options an "omnipresent thread-local global" (like the notion
of the "current NodeManager" was already). Options::current() accesses
this structure.
* Removes Options from constructors and data structures everywhere
(this cleans up a lot of things).
* No longer uses StatisticsRegistry statically. An instance of the
registry is created and linked to a NodeManager.
* StatisticsRegistry::current() is similar to Options::current(), but
the pointer is stowed in the NodeManager (rather than stored)
* The static functions of StatisticsRegistry have been left, for backward
compatibility; they now use the "current" statistics registry.
* SmtEngine::getStatisticsRegistry() is a public accessor for the
registry; this is needed by main() to reach in and get the registry,
for flushing statistics at the end.
|
|
|
|
|
