| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Includes:
- Basic rewriting for choice functions in the builtin rewriter,
- Do not consider more than one equal term in ceg instantiator (helps cases where we have a
repeated pattern of duplicate instantiations),
- Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat
equalities suffice).
- Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass.
|
|
|
|
|
|
|
|
This
makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.
Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default
Allows cbqiNestedQE to be used in the BV logic.
Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).
|
|
* Preprocess extract -> concat pass for cegqi bv.
* Add sygus bench
* Fixes, infrastructure.
* Minor fixes.
* Try
* Minor
* Minor
* Document
* Format
* Improving debug messages.
* Address
* Format
* Overlapping extracts.
* Format
* Minor
* Address review.
* Format
* Comment
* Format
|
|
* Initial setup for preprocessing counterexample lemmas.
* Improve documentation.
* Improving documentation, infrastructure.
* Extraction -> concatentation as a preprocess step.
* Clang format
* Minor
* Make option, refactor effort levels.
* Format
* Clean
* Format
* Rename
* Format
* More
* Format
* Splitting changes.
* Format
* Revert option.
* Minor
* Format
|
|
* Fix some documentation.
* Move model basis out of term db.
* Moving
* Finished moving.
* Document Skolemize and term enumeration.
* Minor
* Model basis to first order model.
* Change function name.
* Minor
* Clang format.
* Minor
* Format
* Minor
* Format
* Address review.
|
|
* Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently.
* Minor
* Make unique bound variables for choice functions in BvInstantor, clean up.
* Incorporate missing optimizations
* Clang format
* Unused field.
* Minor
* Fix, add regression.
* Fix regression.
* Fix bug that led to incorrect cleanup of instantiations.
* Add missing regression
* Improve handling of choice rewriting.
* Fix
* Clang format
* Use canonical variables for choice functions in cbqi bv.
* Add regression
* Clang format.
* Address review.
* Clang format
|
|
* Multi-instantiation heuristic for cbqi bv.
* New clang format.
* Minor
* Minor.
* Minor
|
|
* Initial support for solving bit-vector inequalities in cegqi-bv using conversion to positive equality + model value slack.
* Clang format, remove heuristic.
* Update regressions.
* Simplify interface for CegInstantiator
|
|
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
|
|
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
|
|
* Preparing for bv instantiation, initial working version.
* Undoing bv changes to break up into smaller commit.
|
|
This refactors the apply substitution mechanism for counterexample-guided quantifier instantiation (CEGQI).
Improvements to the code:
(1) Methods have been added to the TermProperties class that summarize their theory-independent behavior (including "getModifiedTerm", "isBasic" etc.). For now, I have not made a "TermPropertiesArith" class yet since this will require more fundamental refactoring.
(2) The terminology "has_coeff" is replaced "is_non_basic" throughout.
(3) Added the applySubstitutionToLiteral method.
(4) Both applySubstitution and applySubstitutionToLiteral are now private within CegInstantiator. This means that theory-specific instantiators do not need to implement custom ways of applying substitutions (previously the arithmetic instantiator was).
(5) applySubstitutionToLiteral is automatically called on all literals (see line 297 of ceg_instantiator.cpp). This means that BvInstantiator::processAssertion is now called on substituted literals. So for instance if our context contains two literals:
x = bv2, bvmul(x,y) = bv4
Say we are asked to solve for x first, and return the substitution {x -> bv2}, then if we are later asked to solve for y, we will call processAssertion for the literal bvmul(bv2,y)=bv4
(6) LIA-specific information "d_theta" in SolvedForm is encapsulated inside the class (with the understanding that this will be made virtual).
This commit has no impact on quantified LIA / LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480
(see CVC4-092217-cegqiRefactorSubs)
|
|
of instantiation for LIA. (#1111)
|
|
* Initial infrastructure for BV instantiation via word-level inversions.
* Minor clean up.
* Change visited to unordered set.
|
|
|
|
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
|
|
|
|
|
|
|
|
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
|
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing
changes made to 5f415d4585134612bc24e9a823289fee35541a01.
|
|
Conflicts:
src/options/quantifiers_options
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
default in EPR mode.
|
|
quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
|
|
|
|
|
|
account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation.
|
|
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
|
|
instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
|
|
|
|
|
|
instantiations. All quantifiers strategies terminate when a conflict can be established.
|
|
|
|
|
|
Breaking an edge between the sat solver and command.h.
|
|
sorts.
|
|
What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.
The Problem:
The build order of CVC4 used to be [roughly] specified as:
options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.
The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.
The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)
The build order of CVC4 can now be [roughly] specified as
base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.
More details about the directories:
base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.
options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .
util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.
expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.
smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.
What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
|
|
|
