summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2017-09-28Cegqi refactor prep bv (#1155)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-27Minor fixes for partial quantifier elimination. (#1147)Andrew Reynolds
2017-09-27CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)Aina Niemetz
2017-09-25Cegqi refactor substitutions (#1129)Andrew Reynolds
2017-09-25Fixing CID 1362917: There was a branch where d_issup was not initialized. Swi...Tim King
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-09-19Refactor cegqi instantiation infrastructure so that it is more independent of...Andrew Reynolds
2017-09-12Initial infrastructure for BV instantiation via word-level inversions. (#1056)Andrew Reynolds
2017-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
2017-08-14Move function defns from smt_engine_scope.h to cpp (#216)Andres Noetzli
2017-08-07Fix compiler warning in theory/quantifiers/term_database_sygus.cppAina Niemetz
2017-08-07Change sygus output for failed reconstruction case.ajreynol
2017-07-31Minor improvement for enumerative instantiation.ajreynol
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-20Fix a few bugs related to sygus.ajreynol
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, cbqi...ajreynol
2017-06-15Fix for issue related to cbqi + E-matching.ajreynol
2017-06-15Fix relevant domain for datatypes, fixes bug 824.ajreynol
2017-06-15Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cb...ajreynol
2017-06-01Minor optimizations related to cbqi.ajreynol
2017-05-20Fix bug 812.ajreynol
2017-05-15Fix bug 806. Minor fixes to remove term formula pass.ajreynol
2017-05-15Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.ajreynol
2017-05-15Make conflict-based instantiation abort if a ground conflict is found in the ...ajreynol
2017-04-28Do not eliminate non-standard arithmetic operators in recursive function defi...ajreynol
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-04-11Bug fix in conjecture generation for --quant-ind.ajreynol
2017-04-05Caching for fun def process, add regression.ajreynol
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ...ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2017-03-30Minor fixes for trigger selection max.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.ajreynol
2017-03-28Minor refactoring sygus.ajreynol
2017-03-28More work on sygus. Add regress4 to Makefile.ajreynol
2017-03-27Making ppNotifyAssertions take a const vector.Tim King
2017-03-24Add some regressions. Minor.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2017-03-22Minor fix for bounded integers.ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring o...ajreynol
2017-03-10Minor fix for cbqi-all.ajreynol
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil no...ajreynol
2017-03-02Fixes related to sets.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback