cvc5.git
12 years agorm something for a future merge that sneaked in
Kshitij Bansal [Wed, 9 May 2012 21:09:31 +0000 (21:09 +0000)]
rm something for a future merge that sneaked in

(gets rid of warning)

12 years agoMerge from decision branch (ITE support)
Kshitij Bansal [Wed, 9 May 2012 05:45:36 +0000 (05:45 +0000)]
Merge from decision branch (ITE support)

Major changes from last merge
* ITEs supported
* Don't share theory lemmas to DE, only assertions

Should probably be noted that 'make regress' doesn't quite
pass with --decision=justification. Throws off search in couple
of arith benchmarks.

No serious performance changes expected. Keep an eye.

12 years agoFixing the debug tags generation and related methods in configuration.cpp that disall...
Dejan Jovanović [Wed, 9 May 2012 03:31:50 +0000 (03:31 +0000)]
Fixing the debug tags generation and related methods in configuration.cpp that disallowed me to debug my bugs by reporting that the debug tag doesn't exists, where in fact it was in the code.

1) The grep and sed for tags wasn't picking up on .isOn("tag")
2) The isDebugTag a) didn't take a parameter b) was using binary search using strcmp which is non-portable and didn't work for tags including special characters

Morgan should vet this, since there is some crazy sed stuff going on

12 years agoMerging in bvprop branch, with proper bit-vector propagation.
Liana Hadarean [Tue, 8 May 2012 21:54:55 +0000 (21:54 +0000)]
Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.

12 years agoFixing a bug with TheoryArith::ppAssert() and shared terms.
Tim King [Mon, 7 May 2012 22:17:35 +0000 (22:17 +0000)]
Fixing a bug with TheoryArith::ppAssert() and shared terms.

12 years agoFixes a sign bug in the DioSolver.
Tim King [Mon, 7 May 2012 22:06:07 +0000 (22:06 +0000)]
Fixes a sign bug in the DioSolver.

12 years agoGuard for expensive Debug trace
Clark Barrett [Fri, 4 May 2012 17:18:02 +0000 (17:18 +0000)]
Guard for expensive Debug trace

12 years agooptions: fail if the debug or trace tag specified doesn't exist (-d -t)
François Bobot [Fri, 4 May 2012 14:28:08 +0000 (14:28 +0000)]
options: fail if the debug or trace tag specified doesn't exist (-d -t)

12 years agofix: getNumTraceTags, getNumDebugTags
François Bobot [Fri, 4 May 2012 14:28:00 +0000 (14:28 +0000)]
fix: getNumTraceTags, getNumDebugTags

12 years ago- This fixes a problem where simplex produced the same conflict in the single check...
Tim King [Fri, 4 May 2012 03:03:34 +0000 (03:03 +0000)]
- This fixes a problem where simplex produced the same conflict in the single check call.
- This increases the number of substitutions that ppAssert can solve on integer equations.

12 years agoSome cleanup starting off from trying to understand the sharing code. Changes include
Dejan Jovanović [Thu, 3 May 2012 20:18:18 +0000 (20:18 +0000)]
Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor

12 years agoChanging d_sharedTermsExist to logicInfo.isSharingEnabled()
Clark Barrett [Wed, 2 May 2012 00:44:40 +0000 (00:44 +0000)]
Changing d_sharedTermsExist to logicInfo.isSharingEnabled()

12 years agoAdded map from skolem variables to new ite formulas in ite removal.
Clark Barrett [Mon, 30 Apr 2012 14:42:28 +0000 (14:42 +0000)]
Added map from skolem variables to new ite formulas in ite removal.
d_sharedTermsExist is now set based on logicInfo instead of dynamically when
shared terms are found.

12 years agoNew LogicInfo functionality.
Morgan Deters [Sat, 28 Apr 2012 01:12:21 +0000 (01:12 +0000)]
New LogicInfo functionality.

src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps
track of which theories are active (which should remain constant throughout
the life of an SmtEngine) and other details (like integers, reals,
linear/nonlinear, etc.).

This class has a default constructor which is the most all-inclusive logic.
Alternatively, this class can be constructed from an SMT-LIB logic string
(the empty string gives the same as "QF_SAT").  Once constructed, theories
can be enabled or disabled, quantifiers flipped on and off, integers flipped
on and off, etc.  At any point an SMT-LIB-like logic string can be extracted.

The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine
(and, in turn, the theories) only a const reference to it.  This ensures that
the logic info doesn't mutate over the course of the run.

As part of this commit, the TheoryEngine's old notion of "active theories"
has been completely removed.  As a result, SMT benchmarks that are incorrectly
tagged with a logic will assert-fail or worse.  (We should probably fail
more gracefully in this case.)  One such example was bug303.smt2,
which used UF reasoning but was tagged QF_LIA.  This has been fixed.

12 years agorequire boost library (but not the threading support---that's only necessary for...
Morgan Deters [Sat, 28 Apr 2012 00:49:10 +0000 (00:49 +0000)]
require boost library (but not the threading support---that's only necessary for portfolio)

12 years agoundo, again
Morgan Deters [Sat, 28 Apr 2012 00:17:03 +0000 (00:17 +0000)]
undo, again

12 years agoadding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration manually...
Morgan Deters [Sat, 28 Apr 2012 00:15:52 +0000 (00:15 +0000)]
adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration manually; this will make the LogicInfo commit coming up much easier to integrate into trunk, and will anyway be cleaned up when quantifiers2 branch is merged into trunk.

12 years agoundo previous commit (as it will break a number of things without additional support...
Morgan Deters [Fri, 27 Apr 2012 23:04:32 +0000 (23:04 +0000)]
undo previous commit (as it will break a number of things without additional support I haven't yet committed)

12 years agoadding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration manually...
Morgan Deters [Fri, 27 Apr 2012 23:03:33 +0000 (23:03 +0000)]
adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration manually; this will make the LogicInfo commit coming up much easier to integrate into trunk, and will anyway be cleaned up when quantifiers2 branch is merged into trunk.

12 years agofix parser logic-handling oversights: QF_UFBV should now be supported
Morgan Deters [Fri, 27 Apr 2012 23:01:29 +0000 (23:01 +0000)]
fix parser logic-handling oversights: QF_UFBV should now be supported

12 years agobreak dependence on zlib-dev for now
Morgan Deters [Fri, 27 Apr 2012 22:07:44 +0000 (22:07 +0000)]
break dependence on zlib-dev for now

12 years agoFixed warning in decision_engine.h, minor tweak to caregraph function in
Clark Barrett [Fri, 27 Apr 2012 19:26:01 +0000 (19:26 +0000)]
Fixed warning in decision_engine.h, minor tweak to caregraph function in
arrays, fixed bug with equalities between constants in shared terms database

12 years agoThis merges in the branch cvc4/branches/arithmetic/matrix into trunk.
Tim King [Fri, 27 Apr 2012 14:47:10 +0000 (14:47 +0000)]
This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!

12 years agoportfolio driver: respect parseOnly option
Kshitij Bansal [Wed, 25 Apr 2012 22:33:00 +0000 (22:33 +0000)]
portfolio driver: respect parseOnly option

12 years agofix for de+lemmas
Kshitij Bansal [Wed, 25 Apr 2012 21:29:49 +0000 (21:29 +0000)]
fix for de+lemmas

for the first time make regress passes even if JH is enabled

12 years agoThis commit merges in the branch branches/arithmetic/congruence into trunk. Here...
Tim King [Tue, 24 Apr 2012 18:36:40 +0000 (18:36 +0000)]
This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager

12 years agoMerge from decision branch -- partially working justification heuristic
Kshitij Bansal [Mon, 23 Apr 2012 17:56:19 +0000 (17:56 +0000)]
Merge from decision branch -- partially working justification heuristic

Overview of changes
* command line option --decision={internal,justification}
* justification heuristic handles all operators except ITEs
  revelant stats: decision::jh::*
* if decisionEngine has solved the problem PropEngine returns
  unknown and smtEngine queries DE to get the answer
  relevant stat: smt::resultSource
* there are known bugs

Full list of commits being merged
r3330 use CD data structures in JH
r3329 add command-line option --decision=MODE
r3328 timer stat, other fixes
r3326 more trace
r3325 enable implies, iff, xor (no further regression losses)
r3324 feed decision engine lemmas, changes to quitting mechanism
r3322 In progress
r3321 more fixes...
r3318 bugfix1 (69 more to go)
r3317 Handle other boolean operators in JH (except ITE)
r3316 mechanism for DE to stopSearch
r3315 merge from trunk + JH translation continuation
r3275 change option to enable JH by default[A

12 years agoUpdates to array theory - much more lazy about introduction of reads
Clark Barrett [Fri, 20 Apr 2012 23:30:08 +0000 (23:30 +0000)]
Updates to array theory - much more lazy about introduction of reads
Also disabled eager lemmas - slows down QF_AX but gets new examples in QF_AUFBV

12 years agoIn the constructor of DecisionEngine, there were 2 pointers that were assumed to...
Tim King [Thu, 19 Apr 2012 18:36:02 +0000 (18:36 +0000)]
In the constructor of DecisionEngine, there were 2 pointers that were assumed to be initialized to NULL. This is not true on all platforms. This is now done explicitly.  Macs builds should now work again.

12 years agoadd the missing BINARY variable in some test/regress makefiles
Kshitij Bansal [Wed, 18 Apr 2012 10:41:45 +0000 (10:41 +0000)]
add the missing BINARY variable in some test/regress makefiles

12 years agocout -> warning. Happening in portfolio
Kshitij Bansal [Wed, 18 Apr 2012 08:41:13 +0000 (08:41 +0000)]
cout -> warning. Happening in portfolio
rest of the search go through, but still should be investigated

12 years agodisabling the problematic pragma in node_manager.h on gcc < 4.6 until we figure out...
Dejan Jovanović [Wed, 18 Apr 2012 01:07:43 +0000 (01:07 +0000)]
disabling the problematic pragma in node_manager.h on gcc < 4.6 until we figure out what to do with it

12 years agoFix for thos annoying "array index" warnings in production builds
Dejan Jovanović [Tue, 17 Apr 2012 20:42:09 +0000 (20:42 +0000)]
Fix for thos annoying "array index" warnings in production builds

12 years agoA dummy decision engine. Expected performance impact: none.
Kshitij Bansal [Tue, 17 Apr 2012 17:20:37 +0000 (17:20 +0000)]
A dummy decision engine. Expected performance impact: none.

Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.

Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin

12 years agoMerges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is...
Tim King [Tue, 17 Apr 2012 16:07:22 +0000 (16:07 +0000)]
Merges branches/arithmetic/atom-database r2979 through 3247 into trunk.  Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
   Roughly speaking this means: (= x (+ y z)) is in normal form.
   (See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
   Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.

12 years agoFixed bug in sharing with arrays of different types
Clark Barrett [Sat, 14 Apr 2012 23:59:17 +0000 (23:59 +0000)]
Fixed bug in sharing with arrays of different types

12 years agoFix SExpr name qualification for swig, and #include integer and rational headers.
Morgan Deters [Fri, 13 Apr 2012 16:21:25 +0000 (16:21 +0000)]
Fix SExpr name qualification for swig, and #include integer and rational headers.

12 years agosvn ignore Makefile.in for aufbv regression directory
Morgan Deters [Thu, 12 Apr 2012 19:30:37 +0000 (19:30 +0000)]
svn ignore Makefile.in for aufbv regression directory

12 years agoAdds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds, an...
Tim King [Thu, 12 Apr 2012 13:26:30 +0000 (13:26 +0000)]
Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds, an Unhandled(SExpr::SexprTypes) could not compile on debian.

12 years agomerge from arrays-clark branch
Morgan Deters [Wed, 11 Apr 2012 16:31:03 +0000 (16:31 +0000)]
merge from arrays-clark branch

12 years ago* Smt2 printer for datatypes
François Bobot [Fri, 6 Apr 2012 22:51:27 +0000 (22:51 +0000)]
* Smt2 printer for datatypes
* Fix DefineFunctionCommand when a constant is defined

12 years ago* Fix ITEs and functions in CVC language printer.
Morgan Deters [Fri, 6 Apr 2012 22:06:52 +0000 (22:06 +0000)]
* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
  internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
  SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)

12 years agofix distributed builds (and therefore the Debian nightly build) by ignoring Makefile...
Morgan Deters [Fri, 6 Apr 2012 20:44:12 +0000 (20:44 +0000)]
fix distributed builds (and therefore the Debian nightly build) by ignoring Makefile.am files under src/prop/cryptominisat.

12 years agoprocessing assertions in bit-vectors even when in fullcheck (needed for sharing)
Dejan Jovanović [Fri, 6 Apr 2012 19:01:25 +0000 (19:01 +0000)]
processing assertions in bit-vectors even when in fullcheck (needed for sharing)

12 years agoSupport to test the "dumper" mechanism in regressions (feeding dump output back in...
Morgan Deters [Thu, 5 Apr 2012 20:07:30 +0000 (20:07 +0000)]
Support to test the "dumper" mechanism in regressions (feeding dump output back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"

12 years agosome settings in bvminisat
Dejan Jovanović [Wed, 4 Apr 2012 16:33:39 +0000 (16:33 +0000)]
some settings in bvminisat

12 years agochanged BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in...
Liana Hadarean [Wed, 4 Apr 2012 14:23:48 +0000 (14:23 +0000)]
changed BVMinisat options to use cc_min=0 in propagate only calls and cc_min=2 in solve

12 years agochanged ccmin_mode in BvMinisat
Liana Hadarean [Wed, 4 Apr 2012 02:46:19 +0000 (02:46 +0000)]
changed ccmin_mode in BvMinisat

12 years ago * added propagation as lemmas to TheoryBV:
Liana Hadarean [Wed, 4 Apr 2012 02:02:06 +0000 (02:02 +0000)]
   * added propagation as lemmas to TheoryBV:
   * modified BVMinisat to work incrementally
   * added more bv regressions

12 years agoFix for make dist.
Tim King [Tue, 3 Apr 2012 15:01:29 +0000 (15:01 +0000)]
Fix for make dist.

12 years agoFix for broken unit tests from the previous commit.
Tim King [Mon, 2 Apr 2012 22:49:39 +0000 (22:49 +0000)]
Fix for broken unit tests from the previous commit.

12 years ago- Merged in the branch cdlist-cleanup.
Tim King [Mon, 2 Apr 2012 20:56:55 +0000 (20:56 +0000)]
- Merged in the branch cdlist-cleanup.
- This adds a CleanUp template argument to CDList.
- CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator.
- CDVector<T> has been simplified and improved.
- The expected performance impact is negligible.

12 years agofix for cvc4_logic dump
Kshitij Bansal [Mon, 2 Apr 2012 20:02:14 +0000 (20:02 +0000)]
fix for cvc4_logic dump

12 years agoRemoving large and unused regress2 benchmarks to decrease the size of checkouts.
Tim King [Mon, 2 Apr 2012 18:56:00 +0000 (18:56 +0000)]
Removing large and unused regress2 benchmarks to decrease the size of checkouts.

12 years agosome more build system fixes
Dejan Jovanović [Fri, 30 Mar 2012 01:46:12 +0000 (01:46 +0000)]
some more build system fixes

12 years agofixing some build systme warnings
Dejan Jovanović [Fri, 30 Mar 2012 01:44:43 +0000 (01:44 +0000)]
fixing some build systme warnings

12 years agoFix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot...
Tim King [Thu, 29 Mar 2012 19:53:20 +0000 (19:53 +0000)]
Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs.

12 years agoFixes a linking problem with the new SatSolverConstructor on Mac.
Tim King [Thu, 29 Mar 2012 19:38:42 +0000 (19:38 +0000)]
Fixes a linking problem with the new SatSolverConstructor on Mac.

12 years agobringing cryptominisat into the main branch
Dejan Jovanović [Thu, 29 Mar 2012 03:08:05 +0000 (03:08 +0000)]
bringing cryptominisat into the main branch

12 years agoenabling the --disable-arithmetic-propagation option in the arithmetic code (it wasn...
Dejan Jovanović [Wed, 28 Mar 2012 19:26:28 +0000 (19:26 +0000)]
enabling the --disable-arithmetic-propagation option in the arithmetic code (it wasn't used)

12 years agofix swig-ignored interface name; hopefully fixes Debian package nightly builds
Morgan Deters [Wed, 28 Mar 2012 18:22:32 +0000 (18:22 +0000)]
fix swig-ignored interface name; hopefully fixes Debian package nightly builds

12 years agoUpdate to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AGAIN...
Tim King [Wed, 28 Mar 2012 17:16:27 +0000 (17:16 +0000)]
Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AGAIN calls.

12 years agoSome renaming and refactoring in SAT
Dejan Jovanović [Wed, 28 Mar 2012 15:44:30 +0000 (15:44 +0000)]
Some renaming and refactoring in SAT

12 years agogetting rid of a rewrite in uf sharing, speeds things up a bit
Dejan Jovanović [Wed, 28 Mar 2012 15:28:38 +0000 (15:28 +0000)]
getting rid of a rewrite in uf sharing, speeds things up a bit

12 years agofixed faulty bv rewrite rule
Liana Hadarean [Wed, 28 Mar 2012 02:47:50 +0000 (02:47 +0000)]
fixed faulty bv rewrite rule

12 years agoadding an extra cache check in the rewriter, speeds things a bit
Dejan Jovanović [Wed, 28 Mar 2012 01:28:08 +0000 (01:28 +0000)]
adding an extra cache check in the rewriter, speeds things a bit
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3828&category=&p=5&reference_id=3820

12 years agoGlobal registry of SAT solvers, where they are registered at compile time. The availa...
Dejan Jovanović [Mon, 26 Mar 2012 19:42:25 +0000 (19:42 +0000)]
Global registry of SAT solvers, where they are registered at compile time. The available SAT solvers can be seen with the --show-sat-solvers option.

12 years agoMore cleaning up.
Dejan Jovanović [Mon, 26 Mar 2012 14:22:38 +0000 (14:22 +0000)]
More cleaning up.

12 years agomore datail from the build failure
Dejan Jovanović [Mon, 26 Mar 2012 12:29:21 +0000 (12:29 +0000)]
more datail from the build failure

12 years agowith a small fix
Dejan Jovanović [Mon, 26 Mar 2012 12:25:12 +0000 (12:25 +0000)]
with a small fix

12 years agoforgot to commit this one, fixing build errors
Dejan Jovanović [Mon, 26 Mar 2012 12:23:54 +0000 (12:23 +0000)]
forgot to commit this one, fixing build errors

12 years agomoving minisat implementation into their respective directories (regular and bv)
Dejan Jovanović [Sun, 25 Mar 2012 20:45:45 +0000 (20:45 +0000)]
moving minisat implementation into their respective directories (regular and bv)

12 years agosat_module.h,cpp -> sat_solver.h,cpp (as intended)
Dejan Jovanović [Sun, 25 Mar 2012 20:12:07 +0000 (20:12 +0000)]
sat_module.h,cpp -> sat_solver.h,cpp (as intended)

12 years agosat.h,cpp -> theory_proxy.h,cpp (this is what it defines)
Dejan Jovanović [Sun, 25 Mar 2012 20:04:43 +0000 (20:04 +0000)]
sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)

12 years agoa cute script to make a video of development from the svn logs
Dejan Jovanović [Sat, 24 Mar 2012 21:18:37 +0000 (21:18 +0000)]
a cute script to make a video of development from the svn logs

12 years agoRemoved the variableRemovalEnabled option and d_removedRows from TheoryArith. This...
Tim King [Fri, 23 Mar 2012 23:06:29 +0000 (23:06 +0000)]
Removed the variableRemovalEnabled option and d_removedRows from TheoryArith.  This had been disabled for several months.

12 years ago* improving arithmetic getEqualityStatus
Dejan Jovanović [Thu, 22 Mar 2012 23:09:03 +0000 (23:09 +0000)]
* improving arithmetic getEqualityStatus
* some sharing improvements based on model

12 years agoMerged updated version of the bitvector theory:
Liana Hadarean [Thu, 22 Mar 2012 21:45:31 +0000 (21:45 +0000)]
Merged updated version of the bitvector theory:
  * added simplification rewrites

12 years agosome improvements to the sharing mechanism/interface
Dejan Jovanović [Thu, 22 Mar 2012 20:40:41 +0000 (20:40 +0000)]
some improvements to the sharing mechanism/interface

12 years agoDisable nonclausal simplification for QF_SAT benchmarks by default.
Morgan Deters [Wed, 21 Mar 2012 20:51:02 +0000 (20:51 +0000)]
Disable nonclausal simplification for QF_SAT benchmarks by default.
(Can be overridden with --simplification=batch, for example.)

12 years agoSome work on the dump infrastructure to support portfolio work.
Morgan Deters [Fri, 9 Mar 2012 21:10:17 +0000 (21:10 +0000)]
Some work on the dump infrastructure to support portfolio work.

  Dump("foo") << FooCommand(...);

now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.

If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run.  This is done even if the muzzle is on.

This commit also cleans up some code that used the dump feature (in arrays,
particularly).

12 years agofix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due to an...
Morgan Deters [Fri, 9 Mar 2012 21:00:51 +0000 (21:00 +0000)]
fix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due to an out-of-place parenthesis

12 years agoStrengthen minisat assertion regarding t-propagations that was unintentionally allowi...
Morgan Deters [Fri, 9 Mar 2012 20:30:15 +0000 (20:30 +0000)]
Strengthen minisat assertion regarding t-propagations that was unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer).  Credit to Clark for finding this.

12 years agominor fixes: to "make dist" in build directories with language bindings enabled;...
Morgan Deters [Fri, 9 Mar 2012 18:26:07 +0000 (18:26 +0000)]
minor fixes: to "make dist" in build directories with language bindings enabled; and to makefile standards conformance

12 years agofix "make dist"
Morgan Deters [Thu, 8 Mar 2012 19:06:08 +0000 (19:06 +0000)]
fix "make dist"

12 years agoFixin the bug Clark found. In final check, enqueued propagations were not discharged.
Dejan Jovanović [Thu, 8 Mar 2012 18:54:02 +0000 (18:54 +0000)]
Fixin the bug Clark found. In final check, enqueued propagations were not discharged.

12 years agoRemoving QUICK_CHECK, and other unused ones, from the Theory::Effort.
Dejan Jovanović [Thu, 8 Mar 2012 02:33:37 +0000 (02:33 +0000)]
Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.

Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions.

Removing one test case from the integer regress0.

12 years agocdqueue : fix size(). Thank you Clark for spotting this silly mistake.
François Bobot [Wed, 7 Mar 2012 22:29:39 +0000 (22:29 +0000)]
cdqueue : fix size(). Thank you Clark for spotting this silly mistake.

12 years agofix some Java compatibility-layer interface problems; also fix some Mac OS X build...
Morgan Deters [Wed, 7 Mar 2012 21:38:04 +0000 (21:38 +0000)]
fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues

12 years agoupdating the equality engine to be able to give explanations for terms that were...
Dejan Jovanović [Tue, 6 Mar 2012 19:08:32 +0000 (19:08 +0000)]
updating the equality engine to be able to give explanations for terms that were not in the databas (queried by areEqual and areDisequal)
and it's a bit better
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731

12 years agoChanging the dependency checking; GMP is required (and sometimes must be explicitly...
Morgan Deters [Sat, 3 Mar 2012 23:29:20 +0000 (23:29 +0000)]
Changing the dependency checking; GMP is required (and sometimes must be explicitly linked in with -l) when using CLN.  Fixes a bug on recent Debian that Francois reported.  Hopefully this doesn't break anything..

12 years agoRemove some commented out code from sat.h
Kshitij Bansal [Fri, 2 Mar 2012 23:43:50 +0000 (23:43 +0000)]
Remove some commented out code from sat.h

12 years agoThis commit merges in the changes from branches/arithmetic/refactor0
Tim King [Fri, 2 Mar 2012 23:37:06 +0000 (23:37 +0000)]
This commit merges in the changes from branches/arithmetic/refactor0
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.

12 years agoCDMap -> CDHashMap
Dejan Jovanović [Fri, 2 Mar 2012 20:38:23 +0000 (20:38 +0000)]
CDMap -> CDHashMap
CDSet -> CDHashSet

12 years agocommitting the TNode/Node fix that was in the kind-backend branch; there's still...
Morgan Deters [Fri, 2 Mar 2012 20:12:44 +0000 (20:12 +0000)]
committing the TNode/Node fix that was in the kind-backend branch; there's still something fishy here, I think I need to merge in a few more things to support incrementality properly.  But this fixes "make check" for now

12 years agoRenamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function...
Tim King [Fri, 2 Mar 2012 16:32:16 +0000 (16:32 +0000)]
Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to function names and documentation.

12 years agoPartial merge from kind-backend branch, including Minisat and CNF work to
Morgan Deters [Thu, 1 Mar 2012 14:48:04 +0000 (14:48 +0000)]
Partial merge from kind-backend branch, including Minisat and CNF work to
support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

12 years agocdqueue2 : cdlist that can be used like queue and can delete element that will never...
François Bobot [Thu, 1 Mar 2012 01:34:35 +0000 (01:34 +0000)]
cdqueue2 : cdlist that can be used like queue and can delete element that will never be restored

12 years agoFixed a copy paste error where a lower bound was looked up instead of an upper bound.
Tim King [Thu, 1 Mar 2012 00:38:37 +0000 (00:38 +0000)]
Fixed a copy paste error where a lower bound was looked up instead of an upper bound.

12 years agoThis should fix the debian build fails:
Liana Hadarean [Wed, 29 Feb 2012 20:33:43 +0000 (20:33 +0000)]
This should fix the debian build fails:
   * removed bvpicosat directory as it is currently not used

Cleared some of the flurry of warnings my previous merge caused in src/prop/