summaryrefslogtreecommitdiff
path: root/src/util/options.cpp
AgeCommit message (Expand)Author
2012-07-31Options merge. This commit:Morgan Deters
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-07-07Various fixes to documentation---typos, some incomplete documentation fixed, ...Morgan Deters
2012-06-22TPTP: add parser for cnf and fofFrançois Bobot
2012-06-17--decision=justification-stoponly : use decision engine only for stoppingKshitij Bansal
2012-06-16changing theoryOf in shared mode with arrays to move equalities to arraysDejan Jovanović
2012-06-14Brings the tuning branch into trunk. This includes the changes from restricte...Tim King
2012-06-12fix ordering issue of --dump-to and --default-dag-thresh. now can be specifi...Morgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-06-09Cleanup and comments for the dag-ifier. Also some unit testing for it.Morgan Deters
2012-06-09Dagification of output expressions.Morgan Deters
2012-06-08The option --arith-presolve-lemmas had previously been renamed --unate-lemmas.Morgan Deters
2012-06-08Merge from decision branch (till r3663)Kshitij Bansal
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-05-30Added BitwiseEq bitvector rewriteClark Barrett
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-17Fixed bug 338:Liana Hadarean
2012-05-14in debug builds, -d can be used for trace tags that aren't also debug tagsMorgan Deters
2012-05-13fixing build warningsDejan Jovanović
2012-05-11Disabled arith-rewrite-equalities by default unless in a pure arithmetic theoryClark Barrett
2012-05-11Added some ITE rewrites,Clark Barrett
2012-05-09--disable-tracing at configure time now disables Trace() and Debug() gestures...Morgan Deters
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-04options: fail if the debug or trace tag specified doesn't exist (-d -t)François Bobot
2012-04-23Merge from decision branch -- partially working justification heuristicKshitij Bansal
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-03-26Global registry of SAT solvers, where they are registered at compile time. Th...Dejan Jovanović
2012-03-23Removed the variableRemovalEnabled option and d_removedRows from TheoryArith....Tim King
2012-03-21Disable nonclausal simplification for QF_SAT benchmarks by default.Morgan Deters
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2012-02-20By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1Morgan Deters
2012-02-16Last commit accidentally lacked r2778 and r2779 from integer2. I have manual...Tim King
2011-11-22More language bindings work:Morgan Deters
2011-11-04STRING_TYPE and CONST_STRING and associate type infrastructure implemented.Morgan Deters
2011-11-02Only print a shortlist of most-commonly-used options on option processing err...Morgan Deters
2011-11-02give an option error if the user specifies --proof in a non-proof-enabled buildMorgan Deters
2011-10-28* ability to output NodeBuilders without first converting them to Nodes---use...Morgan Deters
2011-10-28merged the proofgen3 branch into trunk:Liana Hadarean
2011-10-25Initialize resource limit and millisecond limit optionsKshitij Bansal
2011-10-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
2011-10-04Disabling the variable removal hueristic by default.Tim King
2011-09-30interfaces fixes and cleanups...and examples of each interface!Morgan Deters
2011-09-29compatibility work, documentationMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback