cvc5.git
12 years agospeed up option-file generation on Mac OS by an order of magnitude
Morgan Deters [Mon, 17 Sep 2012 22:38:32 +0000 (22:38 +0000)]
speed up option-file generation on Mac OS by an order of magnitude

12 years agomore bindings fixes
Morgan Deters [Mon, 17 Sep 2012 21:14:37 +0000 (21:14 +0000)]
more bindings fixes

12 years agominor fix for models, added simple cliques option for uf strong solver
Andrew Reynolds [Mon, 17 Sep 2012 16:39:48 +0000 (16:39 +0000)]
minor fix for models, added simple cliques option for uf strong solver

12 years agoenable bug regression for bug 382
Morgan Deters [Sun, 16 Sep 2012 01:24:24 +0000 (01:24 +0000)]
enable bug regression for bug 382

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agostore values returned by get-value in TheoryModel::d_reps if necessary, fixes bug...
Andrew Reynolds [Sun, 16 Sep 2012 00:49:04 +0000 (00:49 +0000)]
store values returned by get-value in TheoryModel::d_reps if necessary, fixes bug 382.

12 years agominor interface improvements, compliance fixes
Morgan Deters [Sat, 15 Sep 2012 22:41:03 +0000 (22:41 +0000)]
minor interface improvements, compliance fixes

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoanother bindings fix (should fix debian build)
Morgan Deters [Sat, 15 Sep 2012 22:32:34 +0000 (22:32 +0000)]
another bindings fix (should fix debian build)

12 years agobug testcase for model generation
Morgan Deters [Sat, 15 Sep 2012 22:27:23 +0000 (22:27 +0000)]
bug testcase for model generation

12 years agoa fix for the java bindings for wei
Morgan Deters [Fri, 14 Sep 2012 19:25:58 +0000 (19:25 +0000)]
a fix for the java bindings for wei

12 years agoFix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).
Morgan Deters [Fri, 14 Sep 2012 17:16:26 +0000 (17:16 +0000)]
Fix a soundness bug reported by Matthias Weiler (had to do with expired TNodes).

Also fix an issue where --check-model didn't take user define-funs into account.

Also make preprocessing a bit more chatty (with -v -v).

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoFix a few minor issues in options processing, improving usability, consistency, error...
Morgan Deters [Fri, 14 Sep 2012 15:13:37 +0000 (15:13 +0000)]
Fix a few minor issues in options processing, improving usability, consistency, error-reporting, and documentation.

12 years agoensure that get-value and get-model are consistent, rewrite function value bodies...
Andrew Reynolds [Thu, 13 Sep 2012 20:39:13 +0000 (20:39 +0000)]
ensure that get-value and get-model are consistent, rewrite function value bodies, do not dag-ify model output

12 years agoAdding model assertions after SAT responses.
Morgan Deters [Wed, 12 Sep 2012 20:31:59 +0000 (20:31 +0000)]
Adding model assertions after SAT responses.

To enable, use --check-models.  Turning on the option can be done in debug or optimized builds, regardless of whether normal assertions are on or not.  This is to allow us to check the generated models in long-running queries, and might be useful to end users as a double-check too.

By default, --check-models is quiet (no output unless it detects a problem).  That allows regression runs to pass unless there are problems:

  make regress CVC4_REGRESSION_ARGS=--check-models

To see it work, use -v in addition to --check-models.

There may still be bugs in the feature itself, but already I've found some apparent model-generation bugs (and discussed with Andy) from this feature, so it seems useful in its current state.

--check-models turns on what SMT-LIBv2 calls "interactive mode" (which keeps the list of user assertions around), and also implies --produce-models.  This version does NOT require incremental-mode, which one design did (the one mentioned in yesterday's meeting).

Also:

* TheoryUF::collectModelInfo() now generates UninterpretedConstants (rather than non-constants)
* The UF rewriter now reduces (APPLY_UF (LAMBDA...) args...), and treats uninterpreted constants correctly (e.g. uc_U_1 != uc_U_2)
* The SubstitutionMap now supports substitutions of operators for paramaterized kinds (e.g., function symbols)

12 years agoadded getCardinality to model
Andrew Reynolds [Tue, 11 Sep 2012 23:44:49 +0000 (23:44 +0000)]
added getCardinality to model

12 years agoPartially reverting the changes made in 4308. There is now both an Expr and Node...
Tim King [Tue, 11 Sep 2012 00:20:51 +0000 (00:20 +0000)]
Partially reverting the changes made in 4308. There is now both an Expr and Node version of getValue() in TheoryModel.

12 years agomodified getValue to return Expr instead of Node
Andrew Reynolds [Mon, 10 Sep 2012 22:29:17 +0000 (22:29 +0000)]
modified getValue to return Expr instead of Node

12 years agoFixed an error in the rewriter Pascal pointed out. This was in effectively dead code...
Tim King [Mon, 10 Sep 2012 20:38:35 +0000 (20:38 +0000)]
Fixed an error in the rewriter Pascal pointed out. This was in effectively dead code. (Nobody internally made minus nodes.)

12 years agolist portfolio_util.h in Makefile, so it gets distributed (fixes debian build)
Morgan Deters [Mon, 10 Sep 2012 14:26:48 +0000 (14:26 +0000)]
list portfolio_util.h in Makefile, so it gets distributed (fixes debian build)

12 years agoAdd [*] footnotes to --help output indicating for many options --FOO that there are...
Morgan Deters [Sat, 8 Sep 2012 23:00:23 +0000 (23:00 +0000)]
Add [*] footnotes to --help output indicating for many options --FOO that there are --no-FOO variants.

12 years agoSome minor changes after reviewing the portfolio "unified driver" commit.
Morgan Deters [Sat, 8 Sep 2012 22:31:44 +0000 (22:31 +0000)]
Some minor changes after reviewing the portfolio "unified driver" commit.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agoSingle driver for both sequential and portfolio
Kshitij Bansal [Sat, 8 Sep 2012 14:25:25 +0000 (14:25 +0000)]
Single driver for both sequential and portfolio

A "command executer" layer between parsing commands and invoking them.

New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.

12 years agoallow SmtEngine::setOption() for trace and debug tags
Morgan Deters [Thu, 6 Sep 2012 22:15:56 +0000 (22:15 +0000)]
allow SmtEngine::setOption() for trace and debug tags

12 years agofixes to the compatibility layer; this fixes the broken system test
Morgan Deters [Thu, 6 Sep 2012 20:05:20 +0000 (20:05 +0000)]
fixes to the compatibility layer; this fixes the broken system test

12 years agoRemove SmtEngine::getStackLevel(), which exposed implementation details and was only...
Morgan Deters [Thu, 6 Sep 2012 02:38:39 +0000 (02:38 +0000)]
Remove SmtEngine::getStackLevel(), which exposed implementation details and was only used by the compatibility layer.

Make SmtEngine::internalPop() delay popping.  This fixes a bug in model generation.

12 years agoadd --incremental to --smtlib2 compliance mode (thanks Peter Collingbourne)
Morgan Deters [Thu, 6 Sep 2012 00:53:18 +0000 (00:53 +0000)]
add --incremental to --smtlib2 compliance mode (thanks Peter Collingbourne)

12 years agoadd a THANKS file for listing external source code contributors
Morgan Deters [Wed, 5 Sep 2012 20:51:34 +0000 (20:51 +0000)]
add a THANKS file for listing external source code contributors

12 years agoAccepted some patches from the Multicore Programming Group at Imperial College London...
Morgan Deters [Tue, 4 Sep 2012 22:22:41 +0000 (22:22 +0000)]
Accepted some patches from the Multicore Programming Group at Imperial College London (via Peter Collingbourne):

cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch
* better checking for cxxtest
cvc4-0002-Do-not-read-an-additional-command-after-failure.patch
* more correct failure behavior for interactive tools
cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch
* don't consider "unsupported" as a failure (accepted with modifications)
cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch
* better get-info responses (accepted with modifications)

These patches will help the group build Boogie support for CVC4.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agominor cleanup leftover from fmf-devel
Andrew Reynolds [Mon, 3 Sep 2012 17:52:07 +0000 (17:52 +0000)]
minor cleanup leftover from fmf-devel

12 years agomerge from fmf-devel branch. more updates to models: now with collectModelInfo with...
Andrew Reynolds [Fri, 31 Aug 2012 16:48:20 +0000 (16:48 +0000)]
merge from fmf-devel branch.  more updates to models: now with collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes.  Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models

12 years agoset the default expression-printing depth to "unlimited"
Morgan Deters [Thu, 30 Aug 2012 21:13:44 +0000 (21:13 +0000)]
set the default expression-printing depth to "unlimited"

12 years ago* Numerous documentation fixes (fix doxygen warnings, add missing documentation,...
Morgan Deters [Wed, 29 Aug 2012 20:36:35 +0000 (20:36 +0000)]
* Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.).

* Remove sat_module.cpp, which was no longer used (was previously refactored?)

12 years agoTo the build system:
Morgan Deters [Wed, 29 Aug 2012 11:50:15 +0000 (11:50 +0000)]
To the build system:

* Fix "make distclean."  This should fix the "local regressions fail"
  that caused documentation, debian, and "distcheck" nightly build targets
  to fail.

* "make clean" now removes some options stuff that previously required a
  "make distclean."

* Cosmetic and portability adjustments.

12 years agotest summaries for automake 1.12 test harness
Morgan Deters [Tue, 28 Aug 2012 18:38:19 +0000 (18:38 +0000)]
test summaries for automake 1.12 test harness

12 years agofix a bug in CLN rational printing where the base was ignored (was causing the new...
Morgan Deters [Tue, 28 Aug 2012 17:14:59 +0000 (17:14 +0000)]
fix a bug in CLN rational printing where the base was ignored (was causing the new CVC3-compatibility-API system test to fail)

12 years agofix regression tests for automake 1.11 and automake 1.12---both versions should work now
Morgan Deters [Tue, 28 Aug 2012 15:26:46 +0000 (15:26 +0000)]
fix regression tests for automake 1.11 and automake 1.12---both versions should work now

12 years agoImproved compatibility layer, now supports quantifiers. Also incorporates
Morgan Deters [Tue, 28 Aug 2012 01:10:16 +0000 (01:10 +0000)]
Improved compatibility layer, now supports quantifiers.  Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.

12 years agofixes for Mac and automake 1.12 detection
Morgan Deters [Tue, 28 Aug 2012 00:44:55 +0000 (00:44 +0000)]
fixes for Mac and automake 1.12 detection

12 years agofix a destruction-order issue that was (1) causing valgrind to complain loudly about...
Morgan Deters [Mon, 27 Aug 2012 20:37:17 +0000 (20:37 +0000)]
fix a destruction-order issue that was (1) causing valgrind to complain loudly about invalid reads and writes, and (2) apparently causing problems deleting the decision engine (which is now being properly deleted)

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years ago* Reversing commit r4258 (which disabled failing regressions). Fixed the problem...
Morgan Deters [Mon, 27 Aug 2012 19:27:28 +0000 (19:27 +0000)]
* Reversing commit r4258 (which disabled failing regressions).  Fixed the problem so they're no longer failing (in the quantifiers rewriter).  Resolves bug #381.

* Added LAMBDA kind and type rule, and Node::isClosure().

(this commit was certified error- and warning-free by the test-and-commit script.)

12 years agominor, lying around in a wd (related to investigating bug 374)
Kshitij Bansal [Sun, 26 Aug 2012 19:53:14 +0000 (19:53 +0000)]
minor, lying around in a wd (related to investigating bug 374)

12 years agodisabling failing regressions
Kshitij Bansal [Sun, 26 Aug 2012 19:39:03 +0000 (19:39 +0000)]
disabling failing regressions

12 years agoArray constants finished and working. Unit tests for array constants.
Clark Barrett [Sun, 26 Aug 2012 17:56:55 +0000 (17:56 +0000)]
Array constants finished and working.  Unit tests for array constants.

12 years agofix unit tests
Morgan Deters [Sat, 25 Aug 2012 21:27:17 +0000 (21:27 +0000)]
fix unit tests

12 years ago* disallow internal uses of mkVar() (you have to mkSkolem())
Morgan Deters [Fri, 24 Aug 2012 23:23:34 +0000 (23:23 +0000)]
* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)

12 years agodisallow assertions to inactive theories.
Morgan Deters [Fri, 24 Aug 2012 23:20:22 +0000 (23:20 +0000)]
disallow assertions to inactive theories.

this fixes at least one known bug where quantifiers could be asserted in quantifier-free logics, with incorrect results.

12 years agofix TheoryEngine::collectModelInfo() to only call collectModelInfo() on active theori...
Morgan Deters [Fri, 24 Aug 2012 21:40:46 +0000 (21:40 +0000)]
fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on active theories; resolves bug 380

12 years agofix warning in arrays rewriter
Morgan Deters [Fri, 24 Aug 2012 01:03:20 +0000 (01:03 +0000)]
fix warning in arrays rewriter

12 years agofix get-value output in a couple ways; this fixes bug #378
Morgan Deters [Fri, 24 Aug 2012 00:29:52 +0000 (00:29 +0000)]
fix get-value output in a couple ways; this fixes bug #378

12 years agoattribute stuff for Clark's array constants
Morgan Deters [Thu, 23 Aug 2012 23:33:52 +0000 (23:33 +0000)]
attribute stuff for Clark's array constants

12 years agoArray constant coding done except for the attributes needed
Clark Barrett [Thu, 23 Aug 2012 18:53:26 +0000 (18:53 +0000)]
Array constant coding done except for the attributes needed

12 years agoCap finite cardinalities at 2^64, as discussed in the meeting last week.
Morgan Deters [Wed, 22 Aug 2012 22:31:59 +0000 (22:31 +0000)]
Cap finite cardinalities at 2^64, as discussed in the meeting last week.

Replace all cardinality comparison functions <=, ==, !=, >=, <, >, with a single compare() function that can return UNKNOWN in the case of unknown (or large-finite and thus not *precisely* known) cardinalities.

12 years agofix some build dependencies in options-building; should fix a strange bug Andy saw...
Morgan Deters [Wed, 22 Aug 2012 20:19:27 +0000 (20:19 +0000)]
fix some build dependencies in options-building; should fix a strange bug Andy saw when adding options & re-making, which was caused by sources not being properly recompiled when they should be

12 years agoMore progress on array constants.
Clark Barrett [Wed, 22 Aug 2012 18:04:10 +0000 (18:04 +0000)]
More progress on array constants.

Here's a fun way to give yourself a week-long headache: try to figure out how
to write efficient code to normalize array constants.

It's mostly there now - just need to figure out how to use type enumerators and
update once the new cardinality stuff is in place.

12 years agoadd some incremental in-tree regressions
Morgan Deters [Tue, 21 Aug 2012 22:13:12 +0000 (22:13 +0000)]
add some incremental in-tree regressions

12 years agorewriterules: fix a correction bug with --simplification=batch
François Bobot [Tue, 21 Aug 2012 20:53:49 +0000 (20:53 +0000)]
rewriterules: fix a correction bug with --simplification=batch

  Rewriterules used ppAssert to obtain early the rewriterules in order
  to use them in ppRewrite. But all the simplifications (ex. f x = b :
  [f x/b]) are not done at that point. Since --simplification=batch
  remove the equality (unlike =incremental), for
  reachability_bbttf_eT_arrays.smt2 the answer was sat instead of
  unsat (thx Andy).

  Partial fix: don't take the rewriterules during ppAssert. That changes
  nothing since early rewrite was already disabled. But the complete
  fix (when early rewrite will be enabled again) will need to take the
  rewriterules more than once.

12 years agoremove duplicate function TheoryEngine::getTheory(TheoryId). It was a duplicate...
Morgan Deters [Mon, 20 Aug 2012 22:01:14 +0000 (22:01 +0000)]
remove duplicate function TheoryEngine::getTheory(TheoryId).  It was a duplicate of TheoryEngine::theoryOf(TheoryId)

12 years agoremoving v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 diffe...
Morgan Deters [Mon, 20 Aug 2012 21:12:00 +0000 (21:12 +0000)]
removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 differ in the answer), so it doesn't really test anything

12 years agominor cleanup
Morgan Deters [Mon, 20 Aug 2012 19:55:33 +0000 (19:55 +0000)]
minor cleanup

12 years agofixes for java bindings
Morgan Deters [Mon, 20 Aug 2012 19:37:30 +0000 (19:37 +0000)]
fixes for java bindings

12 years ago1. Fix for inst_match.cpp to allow compilation on fedora
Clark Barrett [Sun, 19 Aug 2012 02:08:15 +0000 (02:08 +0000)]
1. Fix for inst_match.cpp to allow compilation on fedora
2. Initial implementation of computeIsConst for arrays - still needs
   additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL

12 years agoThe SmtEngine now ensures that setLogicInternal() is called even if there is no expli...
Morgan Deters [Thu, 16 Aug 2012 22:41:07 +0000 (22:41 +0000)]
The SmtEngine now ensures that setLogicInternal() is called even if there is no explicit setLogic().  This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses.  setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.

This means that the CVC language can now take advantage of statistics.

Also added the ability to set the logic from CVC presentation language via (e.g.)
  OPTION "logic" "QF_UFLIA";

Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality.  Kshitij may have a fix (I warned him about this commit).

12 years agobug 374 (was found through fuzzing 2012-07-18)
Kshitij Bansal [Thu, 16 Aug 2012 21:40:41 +0000 (21:40 +0000)]
bug 374 (was found through fuzzing 2012-07-18)

"Possible soundness problem somewhere in the solver
(assertion failure in DE)"

12 years agoReplace propagateAsDecision() with Theory::getNextDecisionRequest():
Morgan Deters [Thu, 16 Aug 2012 21:30:41 +0000 (21:30 +0000)]
Replace propagateAsDecision() with Theory::getNextDecisionRequest():

* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups

12 years agoArrayStoreAll should (for now) only allow constant expressions, as it is itself a...
Morgan Deters [Thu, 16 Aug 2012 19:58:32 +0000 (19:58 +0000)]
ArrayStoreAll should (for now) only allow constant expressions, as it is itself a CONSTANT.

12 years agofix exceptions and mkConst() in java binding
Morgan Deters [Thu, 16 Aug 2012 01:58:41 +0000 (01:58 +0000)]
fix exceptions and mkConst() in java binding

12 years agosome fixes for language bindings
Morgan Deters [Thu, 16 Aug 2012 01:29:19 +0000 (01:29 +0000)]
some fixes for language bindings

12 years agoFixes to integer wrapper classes:
Morgan Deters [Tue, 14 Aug 2012 20:08:29 +0000 (20:08 +0000)]
Fixes to integer wrapper classes:
* more uniform interface between the CLN and GMP wrappers
* support base inference (base == 0) on parsing strings with the CLN wrapper; this was a difference from the GMP wrapper (resolves bug #372)

12 years agoImplements TheoryArith::collectModelInfo(). The current implementation is quite...
Tim King [Tue, 14 Aug 2012 18:01:02 +0000 (18:01 +0000)]
Implements TheoryArith::collectModelInfo().  The current implementation is quite basic. This may need to be revisited.

12 years agoAdds substituteDelta() to DeltaRational which given a value for delta returns the...
Tim King [Tue, 14 Aug 2012 17:55:33 +0000 (17:55 +0000)]
Adds substituteDelta() to DeltaRational which given a value for delta returns the corresponding rational value.

12 years agoSwitched TheoryModel assertEqualityEngine to use const Equality Engine pointers.
Tim King [Tue, 14 Aug 2012 17:52:54 +0000 (17:52 +0000)]
Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.

12 years agoSwitched a number of EqClassIterator operations to const as well as the internal...
Tim King [Tue, 14 Aug 2012 17:50:57 +0000 (17:50 +0000)]
Switched a number of EqClassIterator operations to const as well as the internal EqualityEngine pointer.

12 years agofix integer parsing error.. thanks dejan for the report. this indicates that we...
Morgan Deters [Mon, 13 Aug 2012 20:56:15 +0000 (20:56 +0000)]
fix integer parsing error.. thanks dejan for the report.  this indicates that we have a problem with our Integer class though; it appears to behave differently for GMP and CLN

12 years agoMake a few functions in TheoryEngine (like theoryOf()) const.
Morgan Deters [Mon, 13 Aug 2012 20:47:59 +0000 (20:47 +0000)]
Make a few functions in TheoryEngine (like theoryOf()) const.

12 years agoMinor cleanup. No performance difference expected.
Morgan Deters [Mon, 13 Aug 2012 19:46:27 +0000 (19:46 +0000)]
Minor cleanup.  No performance difference expected.

12 years agominor isConst()-related fixes to printing; also add some debugging stuff to see how...
Morgan Deters [Thu, 9 Aug 2012 13:48:37 +0000 (13:48 +0000)]
minor isConst()-related fixes to printing; also add some debugging stuff to see how isConst() operates: use -d isConst

12 years agoFix --no-checking option.
Morgan Deters [Wed, 8 Aug 2012 22:20:39 +0000 (22:20 +0000)]
Fix --no-checking option.

12 years agoPublic interface review items:
Morgan Deters [Wed, 8 Aug 2012 05:13:53 +0000 (05:13 +0000)]
Public interface review items:

* don't document internal-only stuff (like DefaultCleanup for CDLists)
* NoSuchFunctionException -> TypeCheckingException

12 years agosmall fixes
Dejan Jovanović [Tue, 7 Aug 2012 22:47:22 +0000 (22:47 +0000)]
small fixes

12 years agosome fixes to command and declaration tab-completion in interactive shell
Morgan Deters [Tue, 7 Aug 2012 21:11:16 +0000 (21:11 +0000)]
some fixes to command and declaration tab-completion in interactive shell

12 years agoSome items from the CVC4 public interface review:
Morgan Deters [Tue, 7 Aug 2012 18:38:49 +0000 (18:38 +0000)]
Some items from the CVC4 public interface review:

* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)

12 years agoFix SmtEngine::setInfo() handling for certain keys. This fixes the "unsupported...
Morgan Deters [Tue, 7 Aug 2012 14:53:06 +0000 (14:53 +0000)]
Fix SmtEngine::setInfo() handling for certain keys.  This fixes the "unsupported" message we see in QF_SAT nightly regressions.

12 years agoSupport setting :regular-output-channel and :diagnostic-output-channel.
Morgan Deters [Mon, 6 Aug 2012 22:05:12 +0000 (22:05 +0000)]
Support setting :regular-output-channel and :diagnostic-output-channel.
Also some cleanup of option-related exceptions infrastructure.

12 years agoremoving the sat solver inmterface from being public
Dejan Jovanović [Mon, 6 Aug 2012 21:11:12 +0000 (21:11 +0000)]
removing the sat solver inmterface from being public

12 years agoCleanup of some command stuff, fixes broken Java build.
Morgan Deters [Mon, 6 Aug 2012 19:36:46 +0000 (19:36 +0000)]
Cleanup of some command stuff, fixes broken Java build.

12 years agofix constant printing for datatypes
Dejan Jovanović [Mon, 6 Aug 2012 19:35:39 +0000 (19:35 +0000)]
fix constant printing for datatypes

12 years agoDisable failing datatypes regression, pending solution to bug #370.
Morgan Deters [Sun, 5 Aug 2012 04:41:04 +0000 (04:41 +0000)]
Disable failing datatypes regression, pending solution to bug #370.

12 years agoisConst() rule for datatypes
Morgan Deters [Sat, 4 Aug 2012 18:45:13 +0000 (18:45 +0000)]
isConst() rule for datatypes

12 years agothe array-store "construle" for isConst
Morgan Deters [Fri, 3 Aug 2012 22:38:11 +0000 (22:38 +0000)]
the array-store "construle" for isConst

12 years agoComparisons for LogicInfos, and associated tests
Morgan Deters [Fri, 3 Aug 2012 22:15:33 +0000 (22:15 +0000)]
Comparisons for LogicInfos, and associated tests

12 years agoArrayStoreAll infrastructure
Morgan Deters [Fri, 3 Aug 2012 21:49:20 +0000 (21:49 +0000)]
ArrayStoreAll infrastructure

12 years agofix uses of getMetaKind() from outside the expr package. (they now use isConst(...
Morgan Deters [Fri, 3 Aug 2012 20:39:25 +0000 (20:39 +0000)]
fix uses of getMetaKind() from outside the expr package.  (they now use isConst() and isVar() as appropriate)

also some base infrastructure for the new ::isConst().

12 years agofix for proofs-enabled builds
Morgan Deters [Fri, 3 Aug 2012 18:49:59 +0000 (18:49 +0000)]
fix for proofs-enabled builds

12 years agobetter parser makefile fix
Morgan Deters [Fri, 3 Aug 2012 00:09:57 +0000 (00:09 +0000)]
better parser makefile fix

12 years agofixes to paths in parser makefiles; if you've noticed strange SMT2 parser behavior...
Morgan Deters [Thu, 2 Aug 2012 23:55:08 +0000 (23:55 +0000)]
fixes to paths in parser makefiles; if you've noticed strange SMT2 parser behavior the last couple days, this should fix it

12 years agoarray-store-all class
Morgan Deters [Thu, 2 Aug 2012 21:40:02 +0000 (21:40 +0000)]
array-store-all class

12 years agoadd isFinished() to type enumerators (so we don't rely on exception-throwing after...
Morgan Deters [Wed, 1 Aug 2012 22:33:13 +0000 (22:33 +0000)]
add isFinished() to type enumerators (so we don't rely on exception-throwing after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message

12 years agoa couple fixes to SmtEngine::setOption(). thanks Andy for the report!
Morgan Deters [Wed, 1 Aug 2012 22:17:18 +0000 (22:17 +0000)]
a couple fixes to SmtEngine::setOption().  thanks Andy for the report!

12 years agofixes to some *clean targets
Morgan Deters [Wed, 1 Aug 2012 21:05:36 +0000 (21:05 +0000)]
fixes to some *clean targets

12 years agofix for the SmtEngine::beforeSearch() option predicate
Morgan Deters [Wed, 1 Aug 2012 19:25:10 +0000 (19:25 +0000)]
fix for the SmtEngine::beforeSearch() option predicate

12 years agosome fixes for Mac OS
Morgan Deters [Wed, 1 Aug 2012 02:25:39 +0000 (02:25 +0000)]
some fixes for Mac OS