cvc5.git
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

12 years agofixes for portfolio
Morgan Deters [Tue, 31 Jul 2012 21:44:22 +0000 (21:44 +0000)]
fixes for portfolio

12 years agoMoving some instantiation-related stuff from src/theory to src/theory/quantifiers...
Morgan Deters [Tue, 31 Jul 2012 21:24:31 +0000 (21:24 +0000)]
Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules.  This unclutters the src/theory directory somewhat.

The namespaces weren't changed, only the file locations.

12 years agofix some file documentation
Morgan Deters [Tue, 31 Jul 2012 20:50:24 +0000 (20:50 +0000)]
fix some file documentation

12 years agoOptions merge. This commit:
Morgan Deters [Tue, 31 Jul 2012 20:40:14 +0000 (20:40 +0000)]
Options merge.  This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

12 years agoMinor cleanup after today's commits:
Morgan Deters [Fri, 27 Jul 2012 22:01:03 +0000 (22:01 +0000)]
Minor cleanup after today's commits:

* change some uses of "std::cout" to "Message()"

* change some files to use Unix newlines instead of DOS newlines

* fix compiler warning

12 years agoremoving unecessary files
Andrew Reynolds [Fri, 27 Jul 2012 21:07:42 +0000 (21:07 +0000)]
removing unecessary files

12 years agomerging fmf-devel branch, includes refactored datatype theory, updates to model.h...
Andrew Reynolds [Fri, 27 Jul 2012 19:27:45 +0000 (19:27 +0000)]
merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding.  Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

12 years agoMerge quantifiers2-trunk:
François Bobot [Fri, 27 Jul 2012 13:36:32 +0000 (13:36 +0000)]
Merge quantifiers2-trunk:
   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

12 years agoDatatype enumerator work. This version is not a "fair" enumerator, but I got it...
Morgan Deters [Thu, 26 Jul 2012 21:09:10 +0000 (21:09 +0000)]
Datatype enumerator work.  This version is not a "fair" enumerator, but I got it in quickly for Andy.

A "fair" version forthcoming.

12 years agomore compliance fixes for SMT-LIBv2
Morgan Deters [Wed, 18 Jul 2012 21:32:05 +0000 (21:32 +0000)]
more compliance fixes for SMT-LIBv2

12 years agoa few fixes for java system test
Morgan Deters [Wed, 18 Jul 2012 21:21:56 +0000 (21:21 +0000)]
a few fixes for java system test

12 years agosmall change to model-generation function, after discussion w/ Andy
Morgan Deters [Wed, 18 Jul 2012 21:21:28 +0000 (21:21 +0000)]
small change to model-generation function, after discussion w/ Andy

12 years agoremoving an obsolete assertion in model-generation framework, per Andy's request
Morgan Deters [Wed, 18 Jul 2012 17:37:41 +0000 (17:37 +0000)]
removing an obsolete assertion in model-generation framework, per Andy's request

12 years agoremoving output operator for SExprTypes, which is never used (and SExprTypes is not...
Morgan Deters [Wed, 18 Jul 2012 17:34:12 +0000 (17:34 +0000)]
removing output operator for SExprTypes, which is never used (and SExprTypes is not public-facing)---this fixes the language bindings, which fixes the broken debian build overnight

12 years agoSMT-LIBv2 compliance updates:
Morgan Deters [Tue, 17 Jul 2012 22:07:59 +0000 (22:07 +0000)]
SMT-LIBv2 compliance updates:

* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
  (there were some minor differences from the spec)

12 years agominor fix to prevent getValue from returning null
Andrew Reynolds [Tue, 17 Jul 2012 21:19:58 +0000 (21:19 +0000)]
minor fix to prevent getValue from returning null

12 years agofix for --produce-models with CVC4 presentation language
Morgan Deters [Tue, 17 Jul 2012 21:01:06 +0000 (21:01 +0000)]
fix for --produce-models with CVC4 presentation language

12 years agofix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---but this...
Morgan Deters [Tue, 17 Jul 2012 20:34:34 +0000 (20:34 +0000)]
fix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---but this only gave trouble in strict parsing mode

12 years agonow passes "make distcheck", which does important checks for the release (e.g., ...
Morgan Deters [Mon, 16 Jul 2012 19:00:31 +0000 (19:00 +0000)]
now passes "make distcheck", which does important checks for the release (e.g., "make dist" produces a distribution that passes "make dist" and "make check", "make uninstall" actually uninstalls, "make distclean" actually cleans, ...)

12 years agofix compiler warning in unit test
Morgan Deters [Mon, 16 Jul 2012 17:11:26 +0000 (17:11 +0000)]
fix compiler warning in unit test

12 years agostronger two_smt_engines test
Morgan Deters [Mon, 16 Jul 2012 16:04:56 +0000 (16:04 +0000)]
stronger two_smt_engines test

12 years agofix inadvertent change to system test
Morgan Deters [Mon, 16 Jul 2012 15:53:51 +0000 (15:53 +0000)]
fix inadvertent change to system test

12 years agoSupport for having two SmtEngines with the same ExprManager.
Morgan Deters [Mon, 16 Jul 2012 15:53:22 +0000 (15:53 +0000)]
Support for having two SmtEngines with the same ExprManager.

Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine.  Otherwise, theories register the
same statistic twice.  This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed.  Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).

12 years agofound a bug in the initialization order of UF, EqualityEngine, and the UF strong...
Morgan Deters [Mon, 16 Jul 2012 15:52:36 +0000 (15:52 +0000)]
found a bug in the initialization order of UF, EqualityEngine, and the UF strong solver; fixed

12 years agoreverse the order of link arguments to -lcln -lgmp, fixes linking errors for static...
Morgan Deters [Mon, 16 Jul 2012 15:51:51 +0000 (15:51 +0000)]
reverse the order of link arguments to -lcln -lgmp, fixes linking errors for static-binary CLN-enabled builds on greed

12 years agoType enumerator infrastructure and uninterpreted constant support. No support yet...
Morgan Deters [Sat, 14 Jul 2012 22:53:58 +0000 (22:53 +0000)]
Type enumerator infrastructure and uninterpreted constant support.  No support yet for enumerating arrays, or for enumerating non-trivial datatypes.

12 years agoApplying Dejan's patch for bug #369, which resolves it by adding a new (let..) form...
Morgan Deters [Sat, 14 Jul 2012 21:14:39 +0000 (21:14 +0000)]
Applying Dejan's patch for bug #369, which resolves it by adding a new (let..) form for each introduced binding.

12 years agofixing make dist
Morgan Deters [Sat, 14 Jul 2012 21:04:41 +0000 (21:04 +0000)]
fixing make dist

12 years agofix a warning in unit test compilation
Morgan Deters [Sat, 14 Jul 2012 20:40:00 +0000 (20:40 +0000)]
fix a warning in unit test compilation

12 years agosvn ignore
Morgan Deters [Sat, 14 Jul 2012 17:26:33 +0000 (17:26 +0000)]
svn ignore

12 years agoan example that uses bitvectors to simulate sha1 computation and dumps an smt problem...
Dejan Jovanović [Sat, 14 Jul 2012 13:07:19 +0000 (13:07 +0000)]
an example that uses bitvectors to simulate sha1 computation and dumps an smt problem corresponding to the hash-inversion problem

12 years agoremoving readme from fmf-devel
Andrew Reynolds [Thu, 12 Jul 2012 18:32:08 +0000 (18:32 +0000)]
removing readme from fmf-devel

12 years agomerged fmf-devel branch, includes support for SMT2 command get-value and (extended...
Andrew Reynolds [Thu, 12 Jul 2012 18:30:15 +0000 (18:30 +0000)]
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model.  added collectModelInfo and removed getValue from theory interface.  merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface.  The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

12 years agosvn ingore
Morgan Deters [Tue, 10 Jul 2012 17:58:44 +0000 (17:58 +0000)]
svn ingore