cvc5.git
9 years agosync exerimental scripts with regular ones
Kshitij Bansal [Thu, 4 Jun 2015 17:18:12 +0000 (13:18 -0400)]
sync exerimental scripts with regular ones

9 years agoMinor changes to smt comp script for quantified arith. Add option --cbqi-sat whether...
ajreynol [Thu, 4 Jun 2015 06:14:30 +0000 (08:14 +0200)]
Minor changes to smt comp script for quantified arith.  Add option --cbqi-sat whether to disable sat for quantified arith.

9 years agoexperimental run scripts
Kshitij Bansal [Wed, 3 Jun 2015 22:16:00 +0000 (18:16 -0400)]
experimental run scripts

9 years agorunscript thread stack 256
Kshitij Bansal [Wed, 3 Jun 2015 20:58:39 +0000 (16:58 -0400)]
runscript thread stack 256

9 years agoRefactoring of sygus parsing, properly parse Constant/Variable constructors.
ajreynol [Wed, 3 Jun 2015 11:16:44 +0000 (13:16 +0200)]
Refactoring of sygus parsing, properly parse Constant/Variable constructors.

9 years agoapplication smtcomp
Kshitij Bansal [Tue, 2 Jun 2015 20:40:36 +0000 (16:40 -0400)]
application smtcomp

9 years agoFlatten sygus grammars during parsing. Remove duplicate operators from grammars.
ajreynol [Tue, 2 Jun 2015 17:17:53 +0000 (19:17 +0200)]
Flatten sygus grammars during parsing. Remove duplicate operators from grammars.

9 years agoAdd casc 25 tfn script. Change tff script to output instantiations. Work towards...
ajreynol [Tue, 2 Jun 2015 11:43:51 +0000 (13:43 +0200)]
Add casc 25 tfn script.  Change tff script to output instantiations. Work towards parsing non-flattened sygus grammars.

9 years agoWhen proof enabled, disable uf sym break. Add regression.
ajreynol [Mon, 1 Jun 2015 20:44:40 +0000 (22:44 +0200)]
When proof enabled, disable uf sym break. Add regression.

9 years agoDo not enforce dt fairness when single invocation sygus.
ajreynol [Fri, 29 May 2015 09:47:28 +0000 (11:47 +0200)]
Do not enforce dt fairness when single invocation sygus.

9 years agochanged resource step options to unsigned
lianah [Fri, 29 May 2015 14:18:36 +0000 (10:18 -0400)]
changed resource step options to unsigned

9 years agoadded options for controlling resource step-count for various solving stages
Liana Hadarean [Thu, 28 May 2015 14:03:10 +0000 (15:03 +0100)]
added options for controlling resource step-count for various solving stages

9 years agoMerge pull request #75 from Dunedune/master
lianah [Wed, 27 May 2015 18:25:04 +0000 (19:25 +0100)]
Merge pull request #75 from Dunedune/master

Added missing LogicException to throws in method lemma.

9 years agoAdd missing regression
ajreynol [Mon, 25 May 2015 08:35:00 +0000 (10:35 +0200)]
Add missing regression

9 years agoBug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.
ajreynol [Mon, 25 May 2015 08:34:26 +0000 (10:34 +0200)]
Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.

9 years agoAdded throw LogicException to method lemma.
Jordy Ruiz [Fri, 22 May 2015 08:36:23 +0000 (10:36 +0200)]
Added throw LogicException to method lemma.

9 years agoFixes related to cbqi + E-matching.
ajreynol [Fri, 15 May 2015 17:47:32 +0000 (19:47 +0200)]
Fixes related to cbqi + E-matching.

9 years agoAvoid ensureLiteral on unpreprocessed formulas in cbqi.
ajreynol [Fri, 15 May 2015 07:09:51 +0000 (09:09 +0200)]
Avoid ensureLiteral on unpreprocessed formulas in cbqi.

9 years agoRefactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for...
ajreynol [Wed, 13 May 2015 08:13:16 +0000 (10:13 +0200)]
Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus.

9 years agoAdded Finn Haedicke as a contributor.
Clark Barrett [Tue, 12 May 2015 20:56:00 +0000 (13:56 -0700)]
Added Finn Haedicke as a contributor.

9 years agoMerge pull request #74 from finnhaedicke/namespace_minisat
barrettcw [Tue, 12 May 2015 20:53:34 +0000 (13:53 -0700)]
Merge pull request #74 from finnhaedicke/namespace_minisat

moved Minisat namespace into CVC4

9 years agoAllow sygus with no syntactic restrictions for LIA. Add regressions.
ajreynol [Mon, 11 May 2015 18:06:21 +0000 (20:06 +0200)]
Allow sygus with no syntactic restrictions for LIA.  Add regressions.

9 years agoAdd missing regression.
ajreynol [Mon, 11 May 2015 09:53:07 +0000 (11:53 +0200)]
Add missing regression.

9 years agoSupport for arbitrary constants/variables in Sygus grammars.
ajreynol [Mon, 11 May 2015 09:41:48 +0000 (11:41 +0200)]
Support for arbitrary constants/variables in Sygus grammars.

9 years agoMinor improvements to infrastructure. Minor changes to default options. Add tff scrip...
ajreynol [Sun, 10 May 2015 17:44:58 +0000 (19:44 +0200)]
Minor improvements to infrastructure. Minor changes to default options. Add tff script. Minor additions to sygus.

9 years agoAdd casc25 fnt script.
ajreynol [Fri, 8 May 2015 11:03:41 +0000 (13:03 +0200)]
Add casc25 fnt script.

9 years agoMinor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competitio...
ajreynol [Sat, 2 May 2015 08:13:18 +0000 (10:13 +0200)]
Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competition scripts (in progress).

9 years agoFix smt2 printing of fun-def. Simplification of mbqi interface.
ajreynol [Tue, 28 Apr 2015 13:50:17 +0000 (15:50 +0200)]
Fix smt2 printing of fun-def. Simplification of mbqi interface.

9 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Clark Barrett [Tue, 28 Apr 2015 01:23:54 +0000 (18:23 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

9 years agoFixed problem with private/public header clash
Clark Barrett [Tue, 28 Apr 2015 01:11:29 +0000 (18:11 -0700)]
Fixed problem with private/public header clash

9 years agoDisambiguate namespaces in options, fix permissions
Clark Barrett [Tue, 28 Apr 2015 00:43:10 +0000 (17:43 -0700)]
Disambiguate namespaces in options, fix permissions

9 years agoUpdating failing unit tests.
Tim King [Mon, 27 Apr 2015 11:15:03 +0000 (13:15 +0200)]
Updating failing unit tests.

9 years agoBug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false...
ajreynol [Sun, 26 Apr 2015 17:26:21 +0000 (19:26 +0200)]
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.

9 years agoMore parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi...
ajreynol [Fri, 24 Apr 2015 12:41:28 +0000 (14:41 +0200)]
More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi=gen-ev for interpreted operators.

9 years agoFix sygus parser for non-tokenized operators, reenable regression. Fix for --fmf...
ajreynol [Fri, 24 Apr 2015 08:29:36 +0000 (10:29 +0200)]
Fix sygus parser for non-tokenized operators, reenable regression. Fix for --fmf-fun.

9 years agoFix compiler errors due to unbalanced throw specifiers.
Clark Barrett [Fri, 24 Apr 2015 07:35:08 +0000 (00:35 -0700)]
Fix compiler errors due to unbalanced throw specifiers.

9 years agoMerge branch 'master' into google
Clark Barrett [Thu, 23 Apr 2015 17:45:04 +0000 (10:45 -0700)]
Merge branch 'master' into google

9 years agoWhitespace difference
Clark Barrett [Thu, 23 Apr 2015 17:26:11 +0000 (10:26 -0700)]
Whitespace difference

9 years agoA few more minor updates to match google repository with CVC4 repository
Clark Barrett [Thu, 23 Apr 2015 16:43:52 +0000 (09:43 -0700)]
A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).

9 years agoAdded option for --check-unsat-cores and various core bug fixes (merge of Morgan...
Liana Hadarean [Thu, 23 Apr 2015 16:38:48 +0000 (17:38 +0100)]
Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).

9 years agoMerge pull request #73 from kbansal/parser-dont-tokenize
Kshitij Bansal [Wed, 22 Apr 2015 18:28:58 +0000 (14:28 -0400)]
Merge pull request #73 from kbansal/parser-dont-tokenize

Parser dont tokenize

9 years agoChanges needed to compile at Google, plus some bug fixes from Google.
Clark Barrett [Tue, 21 Apr 2015 23:34:15 +0000 (16:34 -0700)]
Changes needed to compile at Google, plus some bug fixes from Google.

9 years agoFix file permissions
Clark Barrett [Tue, 21 Apr 2015 21:30:51 +0000 (14:30 -0700)]
Fix file permissions

9 years agoFix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
ajreynol [Tue, 21 Apr 2015 14:34:56 +0000 (16:34 +0200)]
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.

9 years agoAdding an example of a tester in SMT2.
Tim King [Tue, 21 Apr 2015 07:55:11 +0000 (09:55 +0200)]
Adding an example of a tester in SMT2.

9 years agoFarkas proof coefficients.
Tim King [Fri, 17 Apr 2015 13:22:53 +0000 (15:22 +0200)]
Farkas proof coefficients.

This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.

Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
  To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
  There was a way to use a row twice in the construction of the conflicts.
  This was violating an assumption in the Tableau when constructing the intermediate rows.

Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
  before they are converted to externally understandable conflicts and propagations in the form
  of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
  to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
  vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
to the impliedByX (and similar functions).
For example,this is now longer both:
  void setAssertedToTheTheory(TNode witness);
  void setAssertedToTheTheoryWithNegationTrue(TNode witness);
  There is just:
    void setAssertedToTheTheory(TNode witness, bool inConflict);

9 years agoPatch for Kshitij's fix on requriePhase
Tianyi Liang [Fri, 17 Apr 2015 19:41:24 +0000 (14:41 -0500)]
Patch for Kshitij's fix on requriePhase

9 years agoMerge pull request #72 from kbansal/decision-requirephase
Kshitij Bansal [Fri, 17 Apr 2015 18:43:20 +0000 (14:43 -0400)]
Merge pull request #72 from kbansal/decision-requirephase

https://www.starexec.org/starexec/secure/details/job.jsp?id=6972

The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.

9 years agomoved Minisat namespace into CVC4
Finn Haedicke [Fri, 17 Apr 2015 08:46:07 +0000 (10:46 +0200)]
moved Minisat namespace into CVC4

This avoids conflicts when CVC4 is linked to an application that
also uses plain Minisat.

9 years agoFix option --quant-fun-wd. Add mk_starexec script to contrib.
ajreynol [Thu, 16 Apr 2015 10:34:27 +0000 (12:34 +0200)]
Fix option --quant-fun-wd.  Add mk_starexec script to contrib.

9 years agoHandle (degenerate) case of synthesis conjectures for constants. Disable delta lemmas.
ajreynol [Thu, 16 Apr 2015 09:21:07 +0000 (11:21 +0200)]
Handle (degenerate) case of synthesis conjectures for constants.  Disable delta lemmas.

9 years agodisable failing sygus tests
Kshitij Bansal [Thu, 16 Apr 2015 04:08:14 +0000 (00:08 -0400)]
disable failing sygus tests

9 years agoupdate comment
Kshitij Bansal [Thu, 16 Apr 2015 04:04:50 +0000 (00:04 -0400)]
update comment

9 years agostring parser builtinop changes
Kshitij Bansal [Thu, 16 Apr 2015 03:59:11 +0000 (23:59 -0400)]
string parser builtinop changes

9 years agobv parserchanges cleanup
Kshitij Bansal [Thu, 16 Apr 2015 03:51:28 +0000 (23:51 -0400)]
bv parserchanges cleanup

9 years agofp builtinop parser changes
Kshitij Bansal [Thu, 16 Apr 2015 03:46:56 +0000 (23:46 -0400)]
fp builtinop parser changes

9 years agofp reorder tokens to match other occurences
Kshitij Bansal [Thu, 16 Apr 2015 03:38:53 +0000 (23:38 -0400)]
fp reorder tokens to match other occurences

9 years agoTHEORY_INTS parser changes
Kshitij Bansal [Thu, 16 Apr 2015 03:34:37 +0000 (23:34 -0400)]
THEORY_INTS parser changes

9 years agoTHEORY_REAL_INTS parser changes
Kshitij Bansal [Thu, 16 Apr 2015 03:31:07 +0000 (23:31 -0400)]
THEORY_REAL_INTS parser changes

9 years agoarray theory builtinop
Kshitij Bansal [Thu, 16 Apr 2015 03:21:52 +0000 (23:21 -0400)]
array theory builtinop

9 years agocleanup
Kshitij Bansal [Thu, 16 Apr 2015 03:00:28 +0000 (23:00 -0400)]
cleanup

9 years agodont tokenize bv operators (normal ones)
Kshitij Bansal [Wed, 4 Mar 2015 20:43:25 +0000 (15:43 -0500)]
dont tokenize bv operators (normal ones)

9 years agoEnabling the regression test: test/regress/regress0/unconstrained/mult1.smt2
Tim King [Wed, 15 Apr 2015 19:34:37 +0000 (21:34 +0200)]
Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2

9 years agoFix for unconstrained bug.
Clark Barrett [Wed, 15 Apr 2015 19:20:13 +0000 (12:20 -0700)]
Fix for unconstrained bug.

9 years agoAdding an example that violates an assertion during unconstrained simplification.
Tim King [Wed, 15 Apr 2015 16:10:43 +0000 (18:10 +0200)]
Adding an example that violates an assertion during unconstrained simplification.

9 years agoMaking CVC4::theory::quantifiers::PrenexQuantMode public for now.
Tim King [Mon, 13 Apr 2015 10:23:49 +0000 (12:23 +0200)]
Making CVC4::theory::quantifiers::PrenexQuantMode public for now.

9 years agodisable string reqressions timing out after change
Kshitij Bansal [Thu, 9 Apr 2015 20:25:01 +0000 (16:25 -0400)]
disable string reqressions timing out after change

9 years agoDE requests respect requirePhase
Kshitij Bansal [Thu, 9 Apr 2015 19:48:25 +0000 (15:48 -0400)]
DE requests respect requirePhase

9 years agoFix unsat-core issues related to rewrite rules, quantifiers preprocessing, and string...
ajreynol [Thu, 9 Apr 2015 13:51:26 +0000 (15:51 +0200)]
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing.  Minor fix for conjecture generation for finite types.

9 years agoFix performance issue with variable triggers + instantiation restrictions.
ajreynol [Thu, 9 Apr 2015 10:43:37 +0000 (12:43 +0200)]
Fix performance issue with variable triggers + instantiation restrictions.

9 years agoBug fix negative contains cache.
ajreynol [Thu, 9 Apr 2015 09:35:33 +0000 (11:35 +0200)]
Bug fix negative contains cache.

9 years agoMake fun-def quantifiers carry the function app they define, make fun-def utilities...
ajreynol [Wed, 8 Apr 2015 10:15:27 +0000 (12:15 +0200)]
Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust.  Fix bug in conjecture generation for non-parameterized operators.

9 years agoRemoving the reference to THEORY_BOOL from the equality engine. This theory
Dejan Jovanovic [Wed, 8 Apr 2015 06:48:57 +0000 (23:48 -0700)]
Removing the reference to THEORY_BOOL from the equality engine. This theory
id was used as an internal marker in a set of theories tagging reasons of a
propagated disequalities. Replaced it with THEORY_LAST which is not completely
kosher but is safe in the context being used.

9 years agoMinor fixes for cegqi.
ajreynol [Tue, 7 Apr 2015 09:37:24 +0000 (11:37 +0200)]
Minor fixes for cegqi.

9 years agoMerge pull request #71 from kbansal/const-are-triggers
Kshitij Bansal [Thu, 2 Apr 2015 17:05:31 +0000 (13:05 -0400)]
Merge pull request #71 from kbansal/const-are-triggers

change const are triggers from false to true in equality engines

Performance comparison:
   https://www.starexec.org/starexec/secure/details/job.jsp?id=6941

Bug opened for testcase that became much worse:
  http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=621

9 years agoImprovements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun-def...
ajreynol [Wed, 1 Apr 2015 11:09:49 +0000 (13:09 +0200)]
Improvements and bug fixes related to cbqi/cegqi.  Minor fix for fmf with fun-def. Add skolemization options.

9 years agofix no return value warning
Kshitij Bansal [Tue, 31 Mar 2015 23:26:27 +0000 (19:26 -0400)]
fix no return value warning

9 years agofix echo command in --tear-down-incremental
Kshitij Bansal [Tue, 31 Mar 2015 23:26:06 +0000 (19:26 -0400)]
fix echo command in --tear-down-incremental

9 years agoprinter change for string smtlib2
Tianyi Liang [Sat, 28 Mar 2015 17:04:33 +0000 (12:04 -0500)]
printer change for string smtlib2

9 years agochange const are triggers from false to true in equality engines
Kshitij Bansal [Wed, 25 Mar 2015 19:04:10 +0000 (15:04 -0400)]
change const are triggers from false to true in equality engines

9 years agoParsing support for define-fun-rec/define-funs-rec.
ajreynol [Mon, 23 Mar 2015 16:54:55 +0000 (17:54 +0100)]
Parsing support for define-fun-rec/define-funs-rec.

9 years agoDecouple counter-example guided quantifier instantiation from Sygus.
ajreynol [Mon, 23 Mar 2015 14:09:25 +0000 (15:09 +0100)]
Decouple counter-example guided quantifier instantiation from Sygus.

9 years agoAdd requirePhase len(x) = 0.
Tianyi Liang [Mon, 16 Mar 2015 16:04:43 +0000 (11:04 -0500)]
Add requirePhase len(x) = 0.

9 years agoFixed proof unitialized memory and minor memory leaks.
Liana Hadarean [Mon, 16 Mar 2015 13:31:21 +0000 (14:31 +0100)]
Fixed proof unitialized memory and minor memory leaks.

9 years agoBug fix for BV
Tianyi Liang [Sat, 14 Mar 2015 22:33:26 +0000 (17:33 -0500)]
Bug fix for BV

9 years agoPatches for 32-bit ARM
Tianyi Liang [Sat, 14 Mar 2015 22:25:17 +0000 (17:25 -0500)]
Patches for 32-bit ARM

9 years agoUpdating resize for occurence lists to properly resize the whole state.
Dejan Jovanovic [Sat, 14 Mar 2015 07:24:24 +0000 (00:24 -0700)]
Updating resize for occurence lists to properly resize the whole state.

9 years agoStrings split on constant lengths, add length=0 to split lemma for empty string.
ajreynol [Wed, 11 Mar 2015 20:11:20 +0000 (21:11 +0100)]
Strings split on constant lengths, add length=0 to split lemma for empty string.

9 years agoMinor fixes and improvements to cegqi-si for linear arithmetic.
ajreynol [Wed, 11 Mar 2015 14:43:56 +0000 (15:43 +0100)]
Minor fixes and improvements to cegqi-si for linear arithmetic.

9 years agoCNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature...
ajreynol [Tue, 10 Mar 2015 14:15:26 +0000 (15:15 +0100)]
CNF proofs.  Infrastructure for preprocessing proofs.  Updates to smt.plf signature.  Add regressions.

9 years agoMinor fixes. Extend cegqi-si to real arithmetic.
ajreynol [Thu, 5 Mar 2015 13:59:15 +0000 (14:59 +0100)]
Minor fixes.  Extend cegqi-si to real arithmetic.

9 years agoMore work on arithmetic single invocation synthesis conjectures.
ajreynol [Wed, 4 Mar 2015 09:39:27 +0000 (10:39 +0100)]
More work on arithmetic single invocation synthesis conjectures.

9 years agoRevert "dummy commit to force nightly builds"
Kshitij Bansal [Sat, 28 Feb 2015 02:47:09 +0000 (21:47 -0500)]
Revert "dummy commit to force nightly builds"

This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.

9 years agoRobust strategy for single invocation LIA synthesis conjectures. Add regressions.
ajreynol [Thu, 26 Feb 2015 14:16:15 +0000 (15:16 +0100)]
Robust strategy for single invocation LIA synthesis conjectures.  Add regressions.

9 years agoSwitch back to eager loop temporarily.
Tianyi Liang [Wed, 25 Feb 2015 16:49:14 +0000 (10:49 -0600)]
Switch back to eager loop temporarily.

9 years agominor fix for internal string print
Tianyi Liang [Wed, 25 Feb 2015 04:13:28 +0000 (22:13 -0600)]
minor fix for internal string print

9 years agoNew trigger options. --inst-no-entail on by default. Misc cleanup.
ajreynol [Sun, 22 Feb 2015 07:59:03 +0000 (08:59 +0100)]
New trigger options.  --inst-no-entail on by default.  Misc cleanup.

9 years agodummy commit to force nightly builds
Kshitij Bansal [Thu, 19 Feb 2015 04:48:35 +0000 (23:48 -0500)]
dummy commit to force nightly builds

9 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Mon, 16 Feb 2015 06:54:31 +0000 (01:54 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

9 years agowebget: curl follow redirect
Kshitij Bansal [Mon, 16 Feb 2015 06:54:27 +0000 (01:54 -0500)]
webget: curl follow redirect