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

12 years ago* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)
Dejan Jovanović [Tue, 10 Jul 2012 15:24:22 +0000 (15:24 +0000)]
* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)
* adding as examples the programs i used to translate nonlinear smt2 problems to other formats

12 years agogoing back to 1. being a non decimal
Dejan Jovanović [Tue, 10 Jul 2012 15:18:32 +0000 (15:18 +0000)]
going back to 1. being a non decimal

12 years agosmall changes:
Dejan Jovanović [Tue, 10 Jul 2012 01:20:44 +0000 (01:20 +0000)]
small changes:
* smtlib2 decimal constant can be "1.", i.e. doesn't need digits after the point
* adding CVC4_PUBLIC to rational output operator, otherwise it's unusable for users

12 years agominor fix-ups
Morgan Deters [Mon, 9 Jul 2012 20:13:23 +0000 (20:13 +0000)]
minor fix-ups

12 years agofix portfolio build
Morgan Deters [Mon, 9 Jul 2012 15:00:37 +0000 (15:00 +0000)]
fix portfolio build

12 years agofix eXecutable bit on a script
Morgan Deters [Mon, 9 Jul 2012 14:54:58 +0000 (14:54 +0000)]
fix eXecutable bit on a script

12 years agominor SMT-LIBv2 compliance issues
Morgan Deters [Sun, 8 Jul 2012 23:45:40 +0000 (23:45 +0000)]
minor SMT-LIBv2 compliance issues

12 years agoremove a debugging line from configure script that was left in inadvertently
Morgan Deters [Sun, 8 Jul 2012 22:10:17 +0000 (22:10 +0000)]
remove a debugging line from configure script that was left in inadvertently

12 years agoanother signed-ness warning fix for newer GCC
Morgan Deters [Sun, 8 Jul 2012 20:55:11 +0000 (20:55 +0000)]
another signed-ness warning fix for newer GCC

12 years agoMinor changes to avoid some warnings on GCC 4.7.1 (Debian wheezy/sid). ANDY - please...
Morgan Deters [Sun, 8 Jul 2012 20:06:22 +0000 (20:06 +0000)]
Minor changes to avoid some warnings on GCC 4.7.1 (Debian wheezy/sid).  ANDY - please look at the diff and make sure I didn't do something stupid

12 years agoBugs resolved by this commit: #314, #322, #359, #364, #365.
Morgan Deters [Sun, 8 Jul 2012 17:36:50 +0000 (17:36 +0000)]
Bugs resolved by this commit: #314, #322, #359, #364, #365.
See below for details.

* Fix the "assert" name-collision bug (resolves bug #364).

  Our identifiers should never be named "assert", as that's a preprocessor
  definition in <assert.h>, which is often #included indirectly (so simply
  having a policy of not including <assert.h> isn't good enough---one of
  our dependences might include it).  It was once the case that we didn't
  have anything named "assert", but "assert()" has now crept back in.
  Instead, name things "assertFoo()" or similar.  Thanks to Tim for the
  report.

  To fix this, I've changed some of Dejan's circuit-propagator code from
  "assert()" to "assertTrue()".  Ditto for Andy's explanation manager.
  Guys, if you prefer a different name in your code, please change it.

* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
  Inner lets now shadow outer lets (previously, they incorrectly gave an
  error).  Additionally, while looking at this, I found that a sequential let
  was implemented rather than a parallel let.  This is now fixed.  Thanks to
  Liana for the report.

* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).

* There were a lot of Debug lines in bitvectors that had embedded toString()
  calls.  This wasted a LOT of time in debug builds for BV benchmarks
  (like in "make regress").  Added if(Debug.isOn(...)) guards; much faster
  now.

* Support for building public-facing interface documentation only (as opposed
  to all internals documentation).  Now "make doc" does the public-facing and
  "make doc-internals" does documentation of everything.  (Along with changes
  to the nightly build script---which will now build and publish both types
  of Doxygen documentation---this resolves bug #359).

* Fix the lambda typechecking bug (resolves bug #322).  Thanks to Andy for the
  report (a long long time ago--sorry).

* The default output language for all streams is now based on the current set
  of Options (if there is one).  This has been a constant annoyance, especially
  when stringstreams are used to construct output.  However, it doesn't work
  for calls from outside the library, so it's mainly an annoyance-fixer for
  CVC4 library code itself.

* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
  are used only in assertions-enabled builds (and thus give warnings in
  production builds).  This was briefly discussed at the meeting this week.

12 years agoVarious fixes to documentation---typos, some incomplete documentation fixed, \file...
Morgan Deters [Sat, 7 Jul 2012 21:01:33 +0000 (21:01 +0000)]
Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.

I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:

  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0

12 years agoAdding std namespace to a couple of make_pair instances.
Tim King [Fri, 6 Jul 2012 17:47:49 +0000 (17:47 +0000)]
Adding std namespace to a couple of make_pair instances.

12 years agoAdded include unistd to main/util.cpp
Tim King [Fri, 6 Jul 2012 17:45:59 +0000 (17:45 +0000)]
Added include unistd to main/util.cpp

12 years agoAdded virtual destructor to PpRewrite.
Tim King [Fri, 6 Jul 2012 17:44:12 +0000 (17:44 +0000)]
Added virtual destructor to PpRewrite.

12 years agoSome changes to configure.ac:
Morgan Deters [Sun, 1 Jul 2012 00:04:49 +0000 (00:04 +0000)]
Some changes to configure.ac:

1. Includes BOOST_CPPFLAGS during compilation of all files, not just portfolio-relevant files.  This is necessary since we now have a general dependence on Boost (not just its threading stuff).  This resolves bug 357.

2. Support --disable-thread-support and --enable-thread-support, in an effort to get to the bottom of bug 361.

These changes shouldn't affect performance, though #1 will build the cvc4 libs with a couple of pthread definitions that conceivably could change the behavior of #included standard headers.  Let's keep an eye on tonight's regressions.

12 years agosvn:ignore
Morgan Deters [Thu, 28 Jun 2012 12:32:05 +0000 (12:32 +0000)]
svn:ignore

12 years agoFixed bug in bv rewriter that caused wrong answer in SMT-COMP
Clark Barrett [Thu, 28 Jun 2012 11:26:07 +0000 (11:26 +0000)]
Fixed bug in bv rewriter that caused wrong answer in SMT-COMP

12 years agofix a link error on church, due to Antlr #defining "true" and "false" :-( --for now...
Morgan Deters [Thu, 28 Jun 2012 09:42:09 +0000 (09:42 +0000)]
fix a link error on church, due to Antlr #defining "true" and "false" :-( --for now, just #undef them after the #include

12 years agoFixing a bug in proof production for the DioSolver.
Tim King [Wed, 27 Jun 2012 22:45:51 +0000 (22:45 +0000)]
Fixing a bug in proof production for the DioSolver.

12 years agoThis adds TheoryArith::safeToReset(). This fixes bug 363.
Tim King [Wed, 27 Jun 2012 21:06:29 +0000 (21:06 +0000)]
This adds TheoryArith::safeToReset().  This fixes bug 363.

12 years agoAdding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorityQueue...
Tim King [Wed, 27 Jun 2012 20:58:37 +0000 (20:58 +0000)]
Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorityQueue::reduce(), ::begin() and ::end().

12 years agoImproved debugging output.
Tim King [Wed, 27 Jun 2012 20:56:23 +0000 (20:56 +0000)]
Improved debugging output.

12 years agoImproved debugging output.
Tim King [Wed, 27 Jun 2012 20:56:04 +0000 (20:56 +0000)]
Improved debugging output.

12 years agoAdding reduce() to the ArithPriorityQueue. This reduces the queue from a superset...
Tim King [Wed, 27 Jun 2012 20:55:17 +0000 (20:55 +0000)]
Adding reduce() to the ArithPriorityQueue. This reduces the queue from a superset of the basic variables that violate a bound to the exact set.

12 years agoAdded a warning to arithmetic for a known dio solver bug. Somehow the fix never made...
Tim King [Mon, 25 Jun 2012 16:00:21 +0000 (16:00 +0000)]
Added a warning to arithmetic for a known dio solver bug. Somehow the fix never made it to trunk. Do not know how. The fix to the bug is pending the hunt for bug 363.

12 years agoTPTP: add parser for cnf and fof
François Bobot [Fri, 22 Jun 2012 15:11:37 +0000 (15:11 +0000)]
TPTP: add parser for cnf and fof
 - include directive works
 - no keyword : 'fof', 'cnf', ... can be used for symbols name
 - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
 - same thing for string

But:
 - string not distinct by projection to real, not sure if the current state of string theory make them distinct
 - filtering in include is not done
 - the result is not printed in the TPTP way (currently SMT2 way)

12 years agoparser: add some acces function and recover the original nextToken from antlr3
François Bobot [Fri, 22 Jun 2012 15:11:21 +0000 (15:11 +0000)]
parser: add some acces function and recover the original nextToken from antlr3
in order to be able to use the stack of streams.

12 years agofix : function AntlrInput::tokenTextSubstr
François Bobot [Fri, 22 Jun 2012 15:11:16 +0000 (15:11 +0000)]
fix : function AntlrInput::tokenTextSubstr

12 years agoParser: add the possibility to bind at level 0.
François Bobot [Fri, 22 Jun 2012 15:11:11 +0000 (15:11 +0000)]
Parser: add the possibility to bind at level 0.

12 years agoqf_lra strategy
Morgan Deters [Mon, 18 Jun 2012 22:43:09 +0000 (22:43 +0000)]
qf_lra strategy

12 years agoReverting buggy rewriter code
Clark Barrett [Mon, 18 Jun 2012 22:39:12 +0000 (22:39 +0000)]
Reverting buggy rewriter code

12 years agoanother qf_lra strategy update
Morgan Deters [Mon, 18 Jun 2012 22:22:04 +0000 (22:22 +0000)]
another qf_lra strategy update

12 years agoFixed bug in rewriter
Clark Barrett [Mon, 18 Jun 2012 22:18:27 +0000 (22:18 +0000)]
Fixed bug in rewriter

12 years agounnecessary ^ in regular expression; warning produced on smt-exec
Morgan Deters [Mon, 18 Jun 2012 21:55:25 +0000 (21:55 +0000)]
unnecessary ^ in regular expression; warning produced on smt-exec

12 years agoQF_LRA strategy in run script, now final (?) for smt-comp 2012
Morgan Deters [Mon, 18 Jun 2012 21:48:02 +0000 (21:48 +0000)]
QF_LRA strategy in run script, now final (?) for smt-comp 2012

12 years agofinal sources (?) for competition
Morgan Deters [Mon, 18 Jun 2012 21:33:00 +0000 (21:33 +0000)]
final sources (?) for competition

12 years agoFix for slow array rewrite and minor bug fix in arrays that popped up as a result
Clark Barrett [Mon, 18 Jun 2012 19:59:56 +0000 (19:59 +0000)]
Fix for slow array rewrite and minor bug fix in arrays that popped up as a result

12 years agosmall bug fix and performance fix in ite simplifier
Clark Barrett [Mon, 18 Jun 2012 16:19:10 +0000 (16:19 +0000)]
small bug fix and performance fix in ite simplifier

12 years agofixed smt version 1 parser for quantifiers
Andrew Reynolds [Mon, 18 Jun 2012 06:04:21 +0000 (06:04 +0000)]
fixed smt version 1 parser for quantifiers

12 years agotracing code to make sure decision options are being set correctly
Kshitij Bansal [Mon, 18 Jun 2012 02:52:11 +0000 (02:52 +0000)]
tracing code to make sure decision options are being set correctly

12 years agobugfix, enable only QF_LRA, not other arith
Kshitij Bansal [Mon, 18 Jun 2012 02:04:37 +0000 (02:04 +0000)]
bugfix, enable only QF_LRA, not other arith

12 years agoQF_LRA, Quantifiers: enable use decision for (only for) stopping search
Kshitij Bansal [Mon, 18 Jun 2012 01:46:39 +0000 (01:46 +0000)]
QF_LRA, Quantifiers: enable use decision for (only for) stopping search

12 years agoFixing bug 360. The driver wasn't exiting when there was an error (it just plowed...
Morgan Deters [Mon, 18 Jun 2012 00:56:27 +0000 (00:56 +0000)]
Fixing bug 360.  The driver wasn't exiting when there was an error (it just plowed ahead to the next command).  Now the driver exits on the first error, unless it's in interactive mode.

12 years agoQF_AUFLIA: enable use decision for (only for) stopping search
Kshitij Bansal [Sun, 17 Jun 2012 23:02:01 +0000 (23:02 +0000)]
QF_AUFLIA: enable use decision for (only for) stopping search

12 years agofixing a problem due to lemmas produced while backtracking
Dejan Jovanović [Sun, 17 Jun 2012 22:33:31 +0000 (22:33 +0000)]
fixing a problem due to lemmas produced while backtracking

12 years ago--decision=justification-stoponly : use decision engine only for stopping
Kshitij Bansal [Sun, 17 Jun 2012 22:04:41 +0000 (22:04 +0000)]
--decision=justification-stoponly : use decision engine only for stopping
search early, not to make decisions

new options.h :)

12 years agoenabling theoryof=term for quantifiers with sharing
Dejan Jovanović [Sun, 17 Jun 2012 18:22:01 +0000 (18:22 +0000)]
enabling theoryof=term for quantifiers with sharing
disableing one test case in equantifiers/decision that runs long

12 years agofixing wrong assertion
Dejan Jovanović [Sun, 17 Jun 2012 16:08:38 +0000 (16:08 +0000)]
fixing wrong assertion

12 years agoRemoved assertion that can fail
Clark Barrett [Sun, 17 Jun 2012 02:29:14 +0000 (02:29 +0000)]
Removed assertion that can fail

12 years agofixing makefile error that brakes build
Dejan Jovanović [Sun, 17 Jun 2012 01:59:53 +0000 (01:59 +0000)]
fixing makefile error that brakes build

12 years agoFix array bug causing incorrect answers
Clark Barrett [Sun, 17 Jun 2012 01:49:58 +0000 (01:49 +0000)]
Fix array bug causing incorrect answers

12 years agosmall change to equality assertions so that one doesn't get x = y and y = x
Dejan Jovanović [Sat, 16 Jun 2012 23:58:07 +0000 (23:58 +0000)]
small change to equality assertions so that one doesn't get x = y and y = x

12 years agoAdding the failing QF_AUFLIA regression mentioned in last commit.
Kshitij Bansal [Sat, 16 Jun 2012 23:04:15 +0000 (23:04 +0000)]
Adding the failing QF_AUFLIA regression mentioned in last commit.
pp-regfile.delta02.smt is the one to look at with
--decision=justificaiton, the delta minimized version of pp-regfile,
which also gives wrong answer. due to various commits/fixes, delta01
gives correct answer currently.

12 years agoThis is an attempt to fix the bug in the justification heuristic. The
Kshitij Bansal [Sat, 16 Jun 2012 22:44:20 +0000 (22:44 +0000)]
This is an attempt to fix the bug in the justification heuristic. The
other minor change is removing dependency of header file in
theory_engine.h

It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a
wrong answer for QF_AUFLIA -- it is currently unclear what is the cause
of this bug, could be sharing.

Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of
course, those for which the answer was wrong earlier; and also perhaps
one or two off-cases)

The issue was with how the infinite loop in justification stuff was prevented.
To keep it short, I skip what was wrong earlier, and this is what is done
now:
* whenever an atomic formula is seen, a list of pairs of <IteSkolemVariable,
  AssertionCorrespondingToIteSkolem> is created for each skolem occuring in
  the atom.
* we iterate over this list, doing the following: check if skolem is marked
  as visited. if not, mark visited, recurse, when back unmark.

I lied, I will tell you what was being done earlier was -- 1. the check for
not being visited was being done in each recursive call, not just for atoms.
2. The AssertionCorrespondingToIteSkolem was being used to check if something
is visited and not IteSkolemVariable. I don't know if this makes any
difference, but anyhow, I think this is cleaner & clearer, so I keep this.

12 years agoupdated build script for smt-comp submission
Morgan Deters [Sat, 16 Jun 2012 22:29:44 +0000 (22:29 +0000)]
updated build script for smt-comp submission