Context-dependent expr attributes are now attached to a specific SmtEngine, and the...
[cvc5.git] / src / smt / smt_engine.cpp
2014-10-14 Morgan DetersContext-dependent expr attributes are now attached...
2014-10-11 Morgan DetersMerge branch '1.4.x'
2014-10-11 Morgan DetersSome defensive programming at destruction time, and...
2014-10-10 Kshitij BansalMerge remote-tracking branch 'origin/1.4.x'
2014-10-09 Morgan DetersMerge branch '1.4.x'
2014-10-07 Morgan DetersMerge branch '1.4.x'
2014-10-06 Morgan DetersMerge branch '1.4.x'
2014-10-06 Morgan DetersMerge branch '1.4.x'
2014-10-06 Morgan DetersSupport for RESET command in CVC native language (and...
2014-10-03 Morgan DetersMerge branch '1.4.x'
2014-10-03 Morgan DetersMerge branch '1.4.x'
2014-10-02 Morgan DetersMerge branch '1.4.x'.
2014-10-02 Morgan DetersFix comment in SmtEngine.
2014-09-30 Morgan DetersMerge branch '1.4.x'
2014-09-30 Morgan DetersProofs- and cores-related segfault fixes (mainly a...
2014-09-27 Morgan DetersMerge branch '1.4.x'
2014-09-26 Morgan DetersMerge branch '1.4.x'
2014-09-17 Kshitij BansalMerge branch '1.4.x' while ignoring commit 8d5eb49.
2014-09-17 Kshitij BansalMerge branch '1.4.x'
2014-09-16 ajreynolRefactoring of conjecture generator. Determine subgoal...
2014-09-03 Kshitij BansalMerge remote-tracking branch 'origin/master'
2014-09-03 ajreynolImplement and enable --dt-var-exp-quant, cleanup trace...
2014-08-29 ajreynolDo not use pure theory terms as single triggers. Minor...
2014-08-26 ajreynolBug fixes for --purify-triggers, --dt-force-assignment.
2014-08-23 Morgan DetersUnsat core printing.
2014-08-23 Morgan DetersSome fixes for dump- and get-unsat-core.
2014-08-22 Morgan DetersOne small thing forgotten in core commit.
2014-08-22 Morgan DetersUnsat core infrastruture and API (SMT-LIB compliance...
2014-08-22 Morgan DetersMerge branch '1.4.x'
2014-08-22 Morgan DetersMerge branch '1.4.x'
2014-08-19 Morgan DetersMerge branch '1.4.x'
2014-08-18 Morgan DetersMerge branch '1.4.x'
2014-08-18 ajreynolAdd support for quantifier-specific instantiation level...
2014-08-15 Kshitij BansalUpdate smt_engine.cpp
2014-07-13 Morgan DetersFix a bug in Boolean terms and arrays. Thanks to Jean...
2014-07-10 Kshitij BansalMerge remote-tracking branch 'origin/master' into segfa...
2014-07-01 Morgan DetersUpdate copyrights.
2014-07-01 Morgan DetersMerge pull request #44 from mdeters/prio-queue-updates
2014-07-01 Morgan DetersMerge pull request #45 from mdeters/turn-off-strings-exp
2014-06-30 Kshitij BansalMerge pull request #47 from kbansal/sets
2014-06-26 Morgan DetersMerge tag 'smtcomp2014-resubmission'
2014-06-25 Andrew ReynoldsMerge pull request #34 from mdeters/datatypes-kinds
2014-06-25 Andrew ReynoldsMerge pull request #37 from mdeters/quants-kinds
2014-06-25 Andrew ReynoldsMerge pull request #38 from mdeters/uf-kinds
2014-06-25 Morgan DetersTurn strings-exp off by default (for the release)
2014-06-23 Morgan DetersFatal error if --unconstrained-simp and --produce-model...
2014-06-22 Morgan DetersMerge tag 'smtcomp2014-application'
2014-06-19 lianahfixed merge conflict
2014-06-19 lianahadded model generation to eager bit-blasting and turned...
2014-06-19 Morgan DetersNew translator features: expand define-funs and combine...
2014-06-19 Morgan DetersFix for new CASC features, fixes Java builds.
2014-06-19 ajreynolFor casc : print models of functions rewritten by sort...
2014-06-17 Morgan DetersNew translator features: expand define-funs and combine...
2014-06-17 Morgan DetersFix for new CASC features, fixes Java builds.
2014-06-17 ajreynolFor casc : print models of functions rewritten by sort...
2014-06-15 lianahEvil bitvector preprocessing pass for simplifying power...
2014-06-13 ajreynolFix handling of ALIA.
2014-06-11 Morgan DetersSome clean-up, post bv-merge.
2014-06-10 Tim KingMerging Tim's pseudoboolean work from his fmcad14 branch.
2014-06-10 lianahMerging CAV14 paper bit-vector work.
2014-06-06 Kshitij BansalMerge pull request #28 from kbansal/sets
2014-06-06 Kshitij BansalSets translate, and other short fixes
2014-06-04 Morgan DetersSmtEngine::checkModel() now checks that model values...
2014-05-15 Andrew ReynoldsMinor fixes. Add SMTCOMP 2014 script.
2014-05-14 Andrew ReynoldsFinish --dump-instantiations option. Update scripts.
2014-05-13 ajreynolAdd lazy strategy for bounded integers to avoid non...
2014-05-12 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-05-11 Andrew ReynoldsMore preparation for CASC proofs. Minor fix for sort...
2014-05-10 Andrew ReynoldsBug fixes to CBQI. Add first draft of CASC j7 TFF...
2014-05-09 Andrew ReynoldsAdd variable ordering to ambqi. Bug fix to macros...
2014-05-02 Andrew ReynoldsAdd option --dt-stc-ind for strengthening skolemization...
2014-05-01 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-30 Tim KingT-entailment work, and QCF (quant conflict find) work...
2014-04-28 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-10 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-04-10 Andrew ReynoldsAdd support for cardinality constraints logic UFC....
2014-04-09 Kshitij BansalMerge pull request #24 from kbansal/sets-model
2014-04-09 Kshitij Bansalfix get-info error-behavior
2014-04-06 Tim KingMerge pull request #21 from pcc/ite-fix
2014-04-03 Morgan DetersSome incremental bugs for Boolean terms, fixed. Thanks...
2014-04-01 Tim KingMerge branch '1.3.x'
2014-03-26 Morgan DetersMerge branch '1.3.x'
2014-03-21 Kshitij BansalMerge pull request #22 from kbansal/sets-model
2014-03-19 Martin BrainRefactor the theory specific parts of definition expans...
2014-03-11 Morgan DetersMerge branch '1.3.x'
2014-03-11 Morgan DetersFix for (get-assignment), resolves bug 553.
2014-03-11 Morgan DetersMerge branch '1.3.x'
2014-03-11 Andrew ReynoldsInitial refactor of rewrite rules, make theory_rewriter...
2014-03-10 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-08 Tim KingMerge remote-tracking branch 'CVC4root/master'
2014-03-08 Morgan DetersRemove --ite-remove-quant; support pulling ground ITEs...
2014-03-08 Morgan DetersFix bug 554 (nominally).
2014-03-07 Morgan DetersFix strings-exp setting.
2014-03-07 Morgan DetersFix strings-exp setting.
2014-03-01 Tianyi Lianga new regular expression engine for solving both positi...
2014-02-28 Tianyi Lianga new regular expression engine for solving both positi...
2014-02-21 Morgan DetersMerge branch '1.3.x'
2014-02-21 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-02-21 Morgan DetersMerge branch '1.3.x'
2014-02-21 Kshitij Bansalportfolio: fix export of emptyset
next