summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
AgeCommit message (Expand)Author
2014-01-18strings with new ideasTianyi Liang
2014-01-16adds partial functionsTianyi Liang
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified formul...Andrew Reynolds
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for in...Andrew Reynolds
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-24Java datatype API fixups, datatype API examplesMorgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-10Whitespace.Morgan Deters
2013-12-10Remove "NodeValue width" outputMorgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-04Partial kind branch merge, including new --rewrite-apply-to-const feature.Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-11-29Fix proofs build.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-20Changing the number of bits allocated per field in node values.Tim King
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-11-04Merge branch 'master' of https://github.com/CVC4/CVC4lianah
2013-10-28Turn off model-based arrays (causing crashes in portfolio)Clark Barrett
2013-10-09fixed options::proof() segfaultlianah
2013-10-09cleaned up proof codelianah
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
2013-10-08added currying for uf proofs; still needs debugginglianah
2013-10-07Multiple fixes for datatypes theory solver: add support for parametric dataty...Andrew Reynolds
2013-10-03Added support for converting unsorted problems to multi-sorted problems via s...Andrew Reynolds
2013-09-30replace with a new method for disequality, move to QF_STianyi Liang
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27Merge branch 'master' of github.com:tiliang/CVC4Morgan Deters
2013-09-27adds communication with arith engineTianyi Liang
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements t...Andrew Reynolds
2013-09-27removes unsound cases, adds unrollingTianyi Liang
2013-09-24Better fix for bug 528Clark Barrett
2013-09-23Revert Clark's last commit, at his request; there are some bugs.Morgan Deters
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
2013-09-19Fix for bug 528Clark Barrett
2013-09-18Fixes to theoryof-mode; no longer static in Theory class.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-09Fix declare-datatypes dumping bug (bug 385).Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se...Morgan Deters
2013-08-20Change recursive expandDefinitions() to an interative worklist-based one; we ...Morgan Deters
2013-08-08Fix a serious bug in the preprocessor; problem inputs reported by Pantazis De...Morgan Deters
2013-07-24Regressions now checking models on unknown too. But quantifiers don't have t...Morgan Deters
2013-07-23(get-info :all-options) to get option values; also command-line option sugges...Morgan Deters
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-25Merge branch '1.2.x'Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback