summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_builder.h
AgeCommit message (Collapse)Author
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
Removing more miscellaneous throw specifiers.
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
* 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.
2017-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
* Move type set to its own file and document. * Move theory engine model builder to its own class. * Working on documentation. * Document Theory Model. * Minor * Document theory model builder. * Clang format * Address review.
2017-07-07Update copyright headers.Mathias Preiner
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ↵ajreynol
Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and ↵ajreynol
--fmf-fun-rlv, fixes bug 723.
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-09-15Refactor setIncomplete in quantifiers.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
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
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵ajreynol
do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
2016-04-20update from the masterPaulMeng
2016-04-03Updating the copyright headers and scripts.Tim King
2015-10-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by ↵ajreynol
default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-04-24Fix compiler errors due to unbalanced throw specifiers.Clark Barrett
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2014-11-13Remove two obsolete versions of MBQI.ajreynol
2014-10-13Model building into quantifiers engine. Simplify axiom-inst mode.ajreynol
2014-07-01Update copyrights.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
* 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
2013-06-28More bug fixes for interval models.Andrew Reynolds
2013-06-25Refactoring of model engine to separate individual implementations of model ↵Andrew Reynolds
builder. Begin work on interval models for integers. Other minor cleanup.
2013-06-17Make --var-elim-quant true by default. Add rewrite engine to quantifiers ↵Andrew Reynolds
module.
2013-05-23Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.Andrew Reynolds
2013-05-22Significant work on bounded integer quantification to handle non-trivial ↵Andrew Reynolds
bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
2013-05-14Refactoring to separate old and new model building/checking code.Andrew Reynolds
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive ↵Andrew Reynolds
miniscoping option --ag-miniscope-quant, minor cleanup
2012-11-02more minor updates to inst gen and representative selection, clean up of ↵Andrew Reynolds
equality query
2012-10-31cleaning up some of the equality query stuff, implemented a new ↵Andrew Reynolds
representative selection strategy for quantifier instantiation
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific ↵Andrew Reynolds
code from quantifiers-specific code
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate ↵Andrew Reynolds
defaults for uf
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of ↵Andrew Reynolds
quantifiers code
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. ↵Andrew Reynolds
cleaned up model code, TheoryModel::getValue is now const.
2012-08-31merge from fmf-devel branch. more updates to models: now with ↵Andrew Reynolds
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-07-31Moving some instantiation-related stuff from src/theory to ↵Morgan Deters
src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat. The namespaces weren't changed, only the file locations.
2012-07-27Minor cleanup after today's commits:Morgan Deters
* change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to ↵Andrew Reynolds
model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback