cvc5.git
12 years agofixes for bug347
Dejan Jovanović [Sun, 10 Jun 2012 03:03:17 +0000 (03:03 +0000)]
fixes for bug347
it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately

12 years agoTurning on unconstrained simp for QF_AUFBV
Clark Barrett [Sat, 9 Jun 2012 17:03:22 +0000 (17:03 +0000)]
Turning on unconstrained simp for QF_AUFBV

12 years agoCleanup and comments for the dag-ifier. Also some unit testing for it.
Morgan Deters [Sat, 9 Jun 2012 14:09:39 +0000 (14:09 +0000)]
Cleanup and comments for the dag-ifier.  Also some unit testing for it.

12 years agoDagification of output expressions.
Morgan Deters [Sat, 9 Jun 2012 00:35:38 +0000 (00:35 +0000)]
Dagification of output expressions.

By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.

If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.

12 years agoThe option --arith-presolve-lemmas had previously been renamed --unate-lemmas.
Morgan Deters [Fri, 8 Jun 2012 23:35:21 +0000 (23:35 +0000)]
The option --arith-presolve-lemmas had previously been renamed --unate-lemmas.

This commit just renames it in --help documentation, etc.

12 years agoExtend Printer infrastructure also to the "Result" class, meaning that different...
Morgan Deters [Fri, 8 Jun 2012 21:21:42 +0000 (21:21 +0000)]
Extend Printer infrastructure also to the "Result" class, meaning that different output languages can write "sat", "unsat", etc., in different ways.  No output is changed by this commit, but the flexibility is added that Francois wanted at today's meeting.

12 years agominor fixes, for Mac OS
Morgan Deters [Fri, 8 Jun 2012 20:11:22 +0000 (20:11 +0000)]
minor fixes, for Mac OS

12 years agovery small fast example for the bv fail
Dejan Jovanović [Fri, 8 Jun 2012 20:00:13 +0000 (20:00 +0000)]
very small fast example for the bv fail

12 years agoFix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).
Morgan Deters [Fri, 8 Jun 2012 19:00:44 +0000 (19:00 +0000)]
Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferring it earlier).

12 years agohandle BitVectorSignExtend in pickler
Kshitij Bansal [Fri, 8 Jun 2012 10:18:01 +0000 (10:18 +0000)]
handle BitVectorSignExtend in pickler

12 years agothreadlocal
Kshitij Bansal [Fri, 8 Jun 2012 09:34:20 +0000 (09:34 +0000)]
threadlocal

12 years agoMerge from decision branch (till r3663)
Kshitij Bansal [Fri, 8 Jun 2012 05:56:08 +0000 (05:56 +0000)]
Merge from decision branch (till r3663)

(no performace or search behavior changes expected)

12 years agosmall fuzz examples where bv fails
Dejan Jovanović [Fri, 8 Jun 2012 05:48:19 +0000 (05:48 +0000)]
small fuzz examples where bv fails

12 years agofixing the wrong results. arrays equality adaptor had a missing case when propagating...
Dejan Jovanović [Thu, 7 Jun 2012 22:19:53 +0000 (22:19 +0000)]
fixing the wrong results. arrays equality adaptor had a missing case when propagating disequalities between shared terms.

12 years agoLogicInfo locking implemented, and some initialization-order issues in SmtEngine...
Morgan Deters [Thu, 7 Jun 2012 20:45:13 +0000 (20:45 +0000)]
LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.

ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers.  In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.

12 years agoFixed performance issue with ite_simplifier on some QF_AUFBV benchmarks
Clark Barrett [Thu, 7 Jun 2012 19:34:21 +0000 (19:34 +0000)]
Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks

12 years agoAdding EchoCommand and associated printer and parser rules:
Morgan Deters [Thu, 7 Jun 2012 16:16:48 +0000 (16:16 +0000)]
Adding EchoCommand and associated printer and parser rules:

* SMT-LIBv2 parser now supports (echo...).
* Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats.
  This can make it much easier to interpret output.

12 years agocleaning up the expample for the future
Dejan Jovanović [Thu, 7 Jun 2012 16:12:06 +0000 (16:12 +0000)]
cleaning up the expample for the future

12 years agoAdded small test case for diseq propagation
Clark Barrett [Thu, 7 Jun 2012 15:31:08 +0000 (15:31 +0000)]
Added small test case for diseq propagation

12 years agofixing some bugs in propagation of disequalities
Dejan Jovanović [Thu, 7 Jun 2012 07:11:24 +0000 (07:11 +0000)]
fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(

12 years agoDon't ever call nonclausalSimplify if simplificationMode = NONE (even if
Clark Barrett [Wed, 6 Jun 2012 21:11:37 +0000 (21:11 +0000)]
Don't ever call nonclausalSimplify if simplificationMode = NONE (even if
repeatSimp is true)

12 years agoFixed assertion failures
Clark Barrett [Wed, 6 Jun 2012 19:29:18 +0000 (19:29 +0000)]
Fixed assertion failures

12 years agoremoving std::cout from trunk
Morgan Deters [Wed, 6 Jun 2012 18:08:28 +0000 (18:08 +0000)]
removing std::cout from trunk

12 years agoalso remove now-incorrect comment from makefile
Morgan Deters [Wed, 6 Jun 2012 17:52:47 +0000 (17:52 +0000)]
also remove now-incorrect comment from makefile

12 years agoFixed broken test case, removed one that is a mistake
Clark Barrett [Wed, 6 Jun 2012 17:49:51 +0000 (17:49 +0000)]
Fixed broken test case, removed one that is a mistake

12 years agounconstrained regressions are now run with "make check", but with --unconstrained...
Morgan Deters [Wed, 6 Jun 2012 17:35:09 +0000 (17:35 +0000)]
unconstrained regressions are now run with "make check", but with --unconstrained-simp option

12 years agoFixing numerous issues with tests and "make dist":
Morgan Deters [Wed, 6 Jun 2012 16:17:19 +0000 (16:17 +0000)]
Fixing numerous issues with tests and "make dist":

* test/regress/regress0/unconstrained wasn't being distributed.  This caused the debian build failure last night.  (It still doesn't run on "make check", but had to be distributed properly.)
* Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format.  (Told automake to use a newer tar format.)

12 years agodisabling a super-expensive assertions to speed up debug runs
Dejan Jovanović [Wed, 6 Jun 2012 16:03:37 +0000 (16:03 +0000)]
disabling a super-expensive assertions to speed up debug runs

12 years agoChanges to the combination mechanism, lots of details. Not done yet, there are still...
Dejan Jovanović [Wed, 6 Jun 2012 06:12:40 +0000 (06:12 +0000)]
Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

12 years agoFixed problem causing crash at destruction time
Clark Barrett [Wed, 6 Jun 2012 01:06:15 +0000 (01:06 +0000)]
Fixed problem causing crash at destruction time

12 years agoMore clean-up
Clark Barrett [Tue, 5 Jun 2012 20:40:22 +0000 (20:40 +0000)]
More clean-up

12 years agoFixed a performance issue with unconstrained simplifier
Clark Barrett [Tue, 5 Jun 2012 19:48:30 +0000 (19:48 +0000)]
Fixed a performance issue with unconstrained simplifier

12 years agoAdding missing files...
Clark Barrett [Tue, 5 Jun 2012 14:43:11 +0000 (14:43 +0000)]
Adding missing files...

12 years agoAdded preprocessing pass that propagates unconstrained values - solves all of
Clark Barrett [Mon, 4 Jun 2012 22:26:40 +0000 (22:26 +0000)]
Added preprocessing pass that propagates unconstrained values - solves all of
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

12 years agoadd a global user-context push/pop in smt engine, just like clark's addition the...
Morgan Deters [Fri, 1 Jun 2012 20:31:24 +0000 (20:31 +0000)]
add a global user-context push/pop in smt engine, just like clark's addition the other day of a push/pop of the sat context

12 years agoFixed bug in bv: one more case where non-shared equality was getting propagated
Clark Barrett [Thu, 31 May 2012 17:15:02 +0000 (17:15 +0000)]
Fixed bug in bv: one more case where non-shared equality was getting propagated
Added a global push and pop around solving - fixes an assertion failure when
TNodes are still around in a CDHashMap at destruction time.

12 years agosvn:ignore a parallel-tests driver file that automake deposits in config/
Morgan Deters [Thu, 31 May 2012 14:46:38 +0000 (14:46 +0000)]
svn:ignore a parallel-tests driver file that automake deposits in config/

12 years agopass JAVA_CPPFLAGS properly
Morgan Deters [Thu, 31 May 2012 14:45:09 +0000 (14:45 +0000)]
pass JAVA_CPPFLAGS properly

12 years agoAdded BitwiseEq bitvector rewrite
Clark Barrett [Wed, 30 May 2012 20:33:40 +0000 (20:33 +0000)]
Added BitwiseEq bitvector rewrite
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times,
twice before ite removal and twice after
Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant
speedup on dwp examples

12 years agoFixed problem with array queue growing too large
Clark Barrett [Wed, 30 May 2012 16:16:18 +0000 (16:16 +0000)]
Fixed problem with array queue growing too large

12 years agoremove unused/broken check build target
Morgan Deters [Wed, 30 May 2012 16:14:56 +0000 (16:14 +0000)]
remove unused/broken check build target

12 years agoremoving now-unused TheoryEngine::setLogic() interface function
Morgan Deters [Tue, 29 May 2012 23:12:06 +0000 (23:12 +0000)]
removing now-unused TheoryEngine::setLogic() interface function

12 years agoEnabled SolveEq bv rewrite
Clark Barrett [Tue, 29 May 2012 17:56:51 +0000 (17:56 +0000)]
Enabled SolveEq bv rewrite

12 years agoAdded some BV rewrites, fixed bugs in array theory, made ite simp work with BV
Clark Barrett [Mon, 28 May 2012 16:27:50 +0000 (16:27 +0000)]
Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV

12 years agosome reordering to keep invariants
Dejan Jovanović [Sun, 27 May 2012 16:59:01 +0000 (16:59 +0000)]
some reordering to keep invariants

12 years agoCommitting the work on equality engine, I need to see how it does on the regressions...
Dejan Jovanović [Sun, 27 May 2012 05:44:13 +0000 (05:44 +0000)]
Committing the work on equality engine, I need to see how it does on the regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes

12 years agoAnother expensive function call in a Debug trace
Clark Barrett [Sun, 27 May 2012 00:39:27 +0000 (00:39 +0000)]
Another expensive function call in a Debug trace

12 years agoAnother expensive function call in a Debug line
Clark Barrett [Sun, 27 May 2012 00:38:30 +0000 (00:38 +0000)]
Another expensive function call in a Debug line

12 years agoinit bug fix
Kshitij Bansal [Fri, 25 May 2012 16:45:21 +0000 (16:45 +0000)]
init bug fix

12 years agoChecking in fix for bug 340 - somehow didn't get checked in earlier
Clark Barrett [Fri, 25 May 2012 00:21:53 +0000 (00:21 +0000)]
Checking in fix for bug 340 - somehow didn't get checked in earlier

12 years agoSeparating the subtheory implementations in the bitvector theory.
Dejan Jovanović [Thu, 24 May 2012 16:03:38 +0000 (16:03 +0000)]
Separating the subtheory implementations in the bitvector theory.

12 years agoSignificant changes to the internals of the equality engine. Equality is not handled...
Dejan Jovanović [Thu, 24 May 2012 05:54:39 +0000 (05:54 +0000)]
Significant changes to the internals of the equality engine. Equality is not handled natively and not as a generic predicate. The changes also change the order of propagation, and can produce different conflicts. Since the engine is now used everywhere this means that so some crazy results are to be expected.

12 years agoThis commit merges in the branch arithmetic/cprop.
Tim King [Tue, 22 May 2012 15:09:03 +0000 (15:09 +0000)]
This commit merges in the branch arithmetic/cprop.

12 years agoUpdating equality manager to handle tagged trigger terms. Notifications are pushed...
Dejan Jovanović [Mon, 21 May 2012 20:15:52 +0000 (20:15 +0000)]
Updating equality manager to handle tagged trigger terms. Notifications are pushed out for relationships between terms tagged with the same tag. No performance impact.

12 years agomain() no longer catches non-CVC4 exceptions. This means on memout and other C+...
Morgan Deters [Mon, 21 May 2012 16:33:53 +0000 (16:33 +0000)]
main() no longer catches non-CVC4 exceptions.  This means on memout and other C++-level exceptions, we'll exit the C++ way rather than our custom way (so we don't get statistics etc.)

12 years agoAdding regress test for bug 341.
Tim King [Sat, 19 May 2012 17:45:37 +0000 (17:45 +0000)]
Adding regress test for bug 341.

12 years ago- The array type rules were fixed to use isSubtypeOf.
Tim King [Sat, 19 May 2012 17:24:52 +0000 (17:24 +0000)]
- The array type rules were fixed to use isSubtypeOf.
- The type of (kind::DIVISION x y) is RealType.
- A reference to util/pseudoboolean.i was removed.
- rec5.cvc is disabled for now.  The type of 2 is Integer which is not a subtype of [0..11].

12 years agoThis commit adds TypeNode::leastCommonTypeNode(). The special case for arithmetic...
Tim King [Fri, 18 May 2012 23:48:38 +0000 (23:48 +0000)]
This commit adds TypeNode::leastCommonTypeNode().  The special case for arithmetic in TypeNode::operator==() has been removed.  A number of faulty type checking checks were switched to use isSubtypeOf. The resolves bug #339

12 years agoThis commit removes the dead psuedoboolean code.
Tim King [Fri, 18 May 2012 20:20:58 +0000 (20:20 +0000)]
This commit removes the dead psuedoboolean code.

12 years agoRemoving long unsigned operator+ from CDList's const_iterator.
Tim King [Fri, 18 May 2012 16:02:50 +0000 (16:02 +0000)]
Removing long unsigned operator+ from CDList's const_iterator.

12 years agoremoving failing regression
Dejan Jovanović [Fri, 18 May 2012 14:24:02 +0000 (14:24 +0000)]
removing failing regression

12 years agoThis fixes a fascinating segfault. This is the sequence of events:
Tim King [Thu, 17 May 2012 23:00:43 +0000 (23:00 +0000)]
This fixes a fascinating segfault.  This is the sequence of events:
1) A restart occurs
2) A shared term is registered to arithmetic.
3) Arithmetic sets this up.
4) No new linear relations are added to arithmetic.
5) Eventually a restart occurs.
6) Arithmetic resets the tableau as it has not had a row added since the last restart.
7) A new variable is added.
8) This exceeds the size of the column vector of the saved tableau by exactly one.
9) segfault

12 years agoFixing an issue with LogicInfo::isPure() that turned off simplification in QF_UF...
Morgan Deters [Thu, 17 May 2012 20:45:32 +0000 (20:45 +0000)]
Fixing an issue with LogicInfo::isPure() that turned off simplification in QF_UF and maybe others

12 years agoFixed bug 338:
Liana Hadarean [Thu, 17 May 2012 18:42:13 +0000 (18:42 +0000)]
Fixed bug 338:
   - fixed buggy rewrite rules assuming certain nodes only had 2 children
   - added support for bv-rewrite dump
   - fixed smt2_printer for bv constants

12 years agoAdding failing regression for ite type computation.
Tim King [Thu, 17 May 2012 15:33:13 +0000 (15:33 +0000)]
Adding failing regression for ite type computation.

12 years agoQueueing up asserted literals in the proxy instead of sending them off to the theory...
Dejan Jovanović [Thu, 17 May 2012 04:34:03 +0000 (04:34 +0000)]
Queueing up asserted literals in the proxy instead of sending them off to the theory engine immediately. The queue is discharged just before a check().

12 years agoadding simple-minded handling of (dis-)equalities where constants are involved
Dejan Jovanović [Wed, 16 May 2012 19:28:25 +0000 (19:28 +0000)]
adding simple-minded handling of (dis-)equalities where constants are involved

12 years agoFixing C compatibility library (it still had a reference to CONST_INTEGER).
Morgan Deters [Wed, 16 May 2012 18:20:09 +0000 (18:20 +0000)]
Fixing C compatibility library (it still had a reference to CONST_INTEGER).

This hopefully fixes the Debian build.

12 years agotestcase for bug 337
Dejan Jovanović [Wed, 16 May 2012 17:54:16 +0000 (17:54 +0000)]
testcase for bug 337

12 years agoChanges to SAT solver:
Dejan Jovanović [Wed, 16 May 2012 17:53:41 +0000 (17:53 +0000)]
Changes to SAT solver:
* allowing propagation of false literals (handles conflict)
* allowing lemmas during BCP (bug 337)
* UF does direct propagation, without checking for literal value anymore

12 years agoequality status for bitvectors can now look into the sat solver to check for IN_MODEL...
Dejan Jovanović [Wed, 16 May 2012 16:18:52 +0000 (16:18 +0000)]
equality status for bitvectors can now look into the sat solver to check for IN_MODEL status

12 years agoremoving duplicate literals in explanations of propagations
Dejan Jovanović [Wed, 16 May 2012 16:01:48 +0000 (16:01 +0000)]
removing duplicate literals in explanations of propagations

12 years agorefactored TheoryBV bitblaster and equality engine into subtheories (similar to Theor...
Liana Hadarean [Wed, 16 May 2012 15:21:18 +0000 (15:21 +0000)]
refactored TheoryBV bitblaster and equality engine into subtheories (similar to TheoryEngine

12 years agofixed QF_BV performance problem due to using CDList instead of CDQueue
Liana Hadarean [Tue, 15 May 2012 22:02:47 +0000 (22:02 +0000)]
fixed QF_BV performance problem due to using CDList instead of CDQueue

12 years ago(no commit message)
Dejan Jovanović [Tue, 15 May 2012 21:58:36 +0000 (21:58 +0000)]

12 years agotest cases
Dejan Jovanović [Tue, 15 May 2012 21:58:09 +0000 (21:58 +0000)]
test cases

12 years agoFix to shared terms visitor.
Tim King [Tue, 15 May 2012 21:20:56 +0000 (21:20 +0000)]
Fix to shared terms visitor.

12 years agoImplement TypeNode::isComparableTo() and add a unit test for it.
Morgan Deters [Tue, 15 May 2012 19:28:18 +0000 (19:28 +0000)]
Implement TypeNode::isComparableTo() and add a unit test for it.

12 years agoFixed several bugs in shared terms database
Clark Barrett [Tue, 15 May 2012 19:24:09 +0000 (19:24 +0000)]
Fixed several bugs in shared terms database

12 years agoThis commit removes the CONST_INTEGER kind from nodes. This code comes from the branc...
Tim King [Tue, 15 May 2012 19:01:19 +0000 (19:01 +0000)]
This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.

12 years agorenamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively
Liana Hadarean [Tue, 15 May 2012 18:53:54 +0000 (18:53 +0000)]
renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively

12 years agoremoving all extended commands (as inspired by the Z3 extended command set) except...
Morgan Deters [Tue, 15 May 2012 18:47:20 +0000 (18:47 +0000)]
removing all extended commands (as inspired by the Z3 extended command set) except for declare-datatypes

12 years agoFix QF_AUFLIA (resolves bug #331).
Morgan Deters [Tue, 15 May 2012 18:22:14 +0000 (18:22 +0000)]
Fix QF_AUFLIA (resolves bug #331).

12 years agofixing warnings, grr
Dejan Jovanović [Tue, 15 May 2012 14:22:34 +0000 (14:22 +0000)]
fixing warnings, grr

12 years agoseveral bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now...
Liana Hadarean [Tue, 15 May 2012 00:11:07 +0000 (00:11 +0000)]
several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328

12 years agofixes for shared term registration. previously the type was not considered when looki...
Dejan Jovanović [Mon, 14 May 2012 20:57:12 +0000 (20:57 +0000)]
fixes for shared term registration. previously the type was not considered when looking at theories of the term and for a term like

read(a, f(x))

the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.

12 years agoFixed assertion failures in array theory
Clark Barrett [Mon, 14 May 2012 19:33:15 +0000 (19:33 +0000)]
Fixed assertion failures in array theory
This fixes bugs 335 and 333.

12 years agoin debug builds, -d can be used for trace tags that aren't also debug tags
Morgan Deters [Mon, 14 May 2012 19:10:39 +0000 (19:10 +0000)]
in debug builds, -d can be used for trace tags that aren't also debug tags

12 years agofixing up preregistration again
Dejan Jovanović [Mon, 14 May 2012 15:13:05 +0000 (15:13 +0000)]
fixing up preregistration again

12 years agofixing build warnings
Dejan Jovanović [Sun, 13 May 2012 15:51:27 +0000 (15:51 +0000)]
fixing build warnings

12 years agofix regex in Debug_tags and Trace_tags generation for Mac OS
Morgan Deters [Fri, 11 May 2012 20:13:28 +0000 (20:13 +0000)]
fix regex in Debug_tags and Trace_tags generation for Mac OS

12 years agofix typo in sed line
Morgan Deters [Fri, 11 May 2012 19:59:04 +0000 (19:59 +0000)]
fix typo in sed line

12 years agooutput a warning message when a function type (or datatype, or array, etc.) is create...
Morgan Deters [Fri, 11 May 2012 19:11:56 +0000 (19:11 +0000)]
output a warning message when a function type (or datatype, or array, etc.) is created with a Boolean term inside it

12 years agoDisabled arith-rewrite-equalities by default unless in a pure arithmetic theory
Clark Barrett [Fri, 11 May 2012 15:20:05 +0000 (15:20 +0000)]
Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory

12 years agoAdded some ITE rewrites,
Clark Barrett [Fri, 11 May 2012 14:00:27 +0000 (14:00 +0000)]
Added some ITE rewrites,
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()

12 years agoPartially fixes something-like-a-problem with TheoryArith::getDeltaValue().
Tim King [Fri, 11 May 2012 01:29:11 +0000 (01:29 +0000)]
Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().

12 years agoRemoving now unneeded (as of r3425) typenames from EqualityEngine. trunk now compiles...
Tim King [Thu, 10 May 2012 14:50:45 +0000 (14:50 +0000)]
Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now compiles on Debian.

12 years agofix an issue which breaks language bindings (so this commit fixes debian nightly...
Morgan Deters [Wed, 9 May 2012 22:40:48 +0000 (22:40 +0000)]
fix an issue which breaks language bindings (so this commit fixes debian nightly builds)

12 years ago--disable-tracing at configure time now disables Trace() and Debug() gestures both.
Morgan Deters [Wed, 9 May 2012 21:52:38 +0000 (21:52 +0000)]
--disable-tracing at configure time now disables Trace() and Debug() gestures both.

12 years ago* simplifying equality engine interface
Dejan Jovanović [Wed, 9 May 2012 21:25:17 +0000 (21:25 +0000)]
* simplifying equality engine interface
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations