projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Add new interfaces to term formula removal and theory preprocess (#5717)
[cvc5.git]
/
test
/
2021-01-05
yoni206
Adding str.len to triggers (#5746)
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Remove quant EPR option (#5716)
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Move slow regression to regress3 (#5715)
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Make theory preprocess rewrite equalities a preprocessi...
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Remove preregister instantiation heuristic (#5713)
tree
|
commitdiff
2020-12-21
Haniel Barbosa
Have unsat core regression agnostic to number of assert...
tree
|
commitdiff
2020-12-21
Andrew Reynolds
Eliminate recursion from the internals of term formula...
tree
|
commitdiff
2020-12-18
Alex Ozdemir
Bugfix: proofs for props of non-normal arith lits ...
tree
|
commitdiff
2020-12-17
Andrew Reynolds
Simplify and fix check models (#5685)
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Simplify preprocessing (#5647)
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Mark quantifier instantiations as needs justify (#5684)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Remove bv divide by zero option (#5672)
tree
|
commitdiff
2020-12-15
Gereon Kremer
Add getters to retrieve constants from api::Term (...
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Properly implement datatype selector triggers (#5624)
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Fix SAT-context dependent issue in strings preregistrat...
tree
|
commitdiff
2020-12-11
yoni206
bv-to-int: new tests from an issue (#5654)
tree
|
commitdiff
2020-12-11
Andrew Reynolds
Fix length assumption for deq norm emp rule (#5623)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Refactor KindMap (#5646)
tree
|
commitdiff
2020-12-10
Aina Niemetz
google test: expr: Migrate node_algorithm_black. (...
tree
|
commitdiff
2020-12-10
Andrew Reynolds
Refactor regressions (#5639)
tree
|
commitdiff
2020-12-10
Aina Niemetz
google test: expr: Migrate kind_black. (#5634)
tree
|
commitdiff
2020-12-09
Aina Niemetz
google test: expr: Migrate kind_map_black. (#5640)
tree
|
commitdiff
2020-12-09
Aina Niemetz
google test: expr: Migrate attribute_white. (#5632)
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Make decision engine independent of AssertionsPipeline...
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Remove obsolete regressions (#5633)
tree
|
commitdiff
2020-12-09
Aina Niemetz
google test: context: Migrate context_white. (#5630)
tree
|
commitdiff
2020-12-09
Aina Niemetz
Delete obsolete unit tests for Expr and ExprManager...
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Ensure CEGQI is applied for parametric datatypes when...
tree
|
commitdiff
2020-12-08
Aina Niemetz
google test: context: Migrate context_mm_black. (#5592)
tree
|
commitdiff
2020-12-08
Aina Niemetz
google test: context: Migrate context_black. (#5587)
tree
|
commitdiff
2020-12-08
Gereon Kremer
Add regression from #1978. (#5552)
tree
|
commitdiff
2020-12-08
Abdalrhman Mohamed
Fix a bug with synth-fun printer (#5512)
tree
|
commitdiff
2020-12-08
yoni206
bv-to-int: Expand definitions of bvudiv and bvurem...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Make term indices in the strings base solver aware...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Proper implementation of expand definitions for sequenc...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Fix collect model values for sequences of sequences...
tree
|
commitdiff
2020-12-08
Mathias Preiner
Disable algebraic BV subtheory by default and make...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Fix and reenable fact vs lemma optimization in datatype...
tree
|
commitdiff
2020-12-07
makaimann
Add bitwise refinement mode for IAND (#5328)
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Fix issue with free variables introduced by quantifier...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-07
Gereon Kremer
Add regression from #4927 (#5556)
tree
|
commitdiff
2020-12-04
Aina Niemetz
google test: expr: Migrate attribute_black. (#5598)
tree
|
commitdiff
2020-12-04
Aina Niemetz
google test: context: Migrate cdo_black. (#5586)
tree
|
commitdiff
2020-12-04
Aina Niemetz
google test: context: Migrate cdmap_white. (#5585)
tree
|
commitdiff
2020-12-04
Aina Niemetz
google test: api: Migrate sort_black. (#5594)
tree
|
commitdiff
2020-12-04
Aina Niemetz
google test: context: Migrate cdmap_black. (#5584)
tree
|
commitdiff
2020-12-04
Aina Niemetz
google test: context: Migrate cdlist_black. (#5582)
tree
|
commitdiff
2020-12-03
Aina Niemetz
google test: api: Migrate solver_black. (#5570)
tree
|
commitdiff
2020-12-03
Gereon Kremer
Use mkAnd where the number of children may be less...
tree
|
commitdiff
2020-12-03
yoni206
Models as (#5581)
tree
|
commitdiff
2020-12-03
Aina Niemetz
google test: Add fixture for context tests. (#5590)
tree
|
commitdiff
2020-12-03
Gereon Kremer
Make run_regression.py executable. (#5588)
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-03
Aina Niemetz
google test: base: Migrate map_util_black. (#5580)
tree
|
commitdiff
2020-12-02
Aina Niemetz
Fix RoundingMode mapping in API. (#5578)
tree
|
commitdiff
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
tree
|
commitdiff
2020-12-02
Aina Niemetz
google test: api: Migrate term_black. (#5571)
tree
|
commitdiff
2020-12-02
Aina Niemetz
google test: api: Use individual fixture for datatype_b...
tree
|
commitdiff
2020-12-02
Aina Niemetz
google test: api: Migrate op_black. (#5567)
tree
|
commitdiff
2020-12-02
Aina Niemetz
google test: api: Migrate grammar_black. (#5566)
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Use new let binding for cvc printer (#5561)
tree
|
commitdiff
2020-12-02
Gereon Kremer
Add regressions from #3687. (#5553)
tree
|
commitdiff
2020-12-02
Aina Niemetz
google test: api: Migrate result_black. (#5569)
tree
|
commitdiff
2020-12-02
Aina Niemetz
google test: Infrastructure and first api test. (#5548)
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Fix issues related to model declarations (#5560)
tree
|
commitdiff
2020-12-01
Andres Noetzli
Improve rewriting of str.<= (#4848)
tree
|
commitdiff
2020-12-01
Gereon Kremer
Add regressions from #5099 (#5557)
tree
|
commitdiff
2020-12-01
Gereon Kremer
Add regression for #4335. (#5554)
tree
|
commitdiff
2020-12-01
Gereon Kremer
Add regressions for #4707. (#5555)
tree
|
commitdiff
2020-12-01
Andrew Reynolds
More fixes for quantifier elimination (#5533)
tree
|
commitdiff
2020-12-01
yoni206
fix metadata for a test (#5546)
tree
|
commitdiff
2020-11-26
Gereon Kremer
Make CAD solver work for empty set of assertions (...
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Fully decouple SmtEngine and the Expr layer (#5532)
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Disable fact vs lemma optimization in datatypes for...
tree
|
commitdiff
2020-11-25
Andrew Reynolds
Add regressions for closed issues (#5526)
tree
|
commitdiff
2020-11-25
Andrew Reynolds
Use symbol manager for printing responses get-model...
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Fix regular expression consume for nested star (#5518)
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Change UF ho to ppRewrite instead of expand definition...
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Fix quantifiers scope issue in strings preprocessor...
tree
|
commitdiff
2020-11-21
mudathirmahgoub
Add posRewriteEqual to bags rewriter (#5498)
tree
|
commitdiff
2020-11-20
Andrew Reynolds
Fix remove term formula policy for terms beneath quanti...
tree
|
commitdiff
2020-11-20
Andrew Reynolds
Support nested quantifier elimination for get-qe comman...
tree
|
commitdiff
2020-11-20
Andrew Reynolds
Updates to API in preparation for using symbol manager...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Enable new implementation of CEGQI based on nested...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Use new let binding utility in smt2 printer (#5472)
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Fix issues related to eliminating extended arithmetic...
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Disable slow nl regression (#5467)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Do not expand definitions of extended arithmetic operat...
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Use symbol manager for get assignment (#5451)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Fix asan issues related to solver and symbol manager...
tree
|
commitdiff
2020-11-14
Andrew Reynolds
Fix double conflict in extended string solver (#5435)
tree
|
commitdiff
2020-11-13
Andrew Reynolds
Make regular expression difference left associative...
tree
|
commitdiff
2020-11-12
yoni206
Models standard (#5415)
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Move symbol manager to src/expr/ (#5420)
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Pass symbol manager to commands (#5410)
tree
|
commitdiff
2020-11-11
Andrew Reynolds
Fix preregistration in TheorySep before declare-heap...
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Do not mark extended functions as reduced based on...
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Add proper support for the declare-heap command for...
tree
|
commitdiff
2020-11-09
Andrew Reynolds
Add symbol manager (#5380)
tree
|
commitdiff
next