Age | Commit message (Collapse) | Author |
|
|
|
works).
|
|
|
|
|
|
the report.
|
|
|
|
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
|
|
driver except in interactive mode.
|
|
bug.
|
|
-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.
- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.
- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.
Minor Changes:
- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.
- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.
-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.
- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
model info. Also fix bug in model post-processor.
|
|
|
|
datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly. Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
|
|
sort inference and monotonicity. Minor cleanup.
|
|
|
|
|
|
|
|
|
|
to bounded integer quantifier instantiation.
|
|
|
|
|
|
This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.
|
|
for faster compilation
|
|
|
|
|
|
|
|
|
|
|
|
|
|
segfault in smt2 printer
|
|
were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
|
|
Deligiannis.
|
|
|
|
to be simplified by check-model in that case.
|
|
|
|
suggestions
|
|
|
|
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.
|
|
|
|
|
|
|
|
allows linearization of div,mod,/ by a constant.
|