projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Add missing stat for lemmas based on inferences (#4214)
2020-03-03
Andrew Reynolds
Standardize the interface for SMT engine subsolvers...
commit
|
commitdiff
|
tree
2020-03-02
Andrew Reynolds
Split collect model info by types in strings (#3847)
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Convert more uses of string to word (#3834)
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Throw warning instead of error for non-constant values...
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Fix assertion related to assignability in the model...
commit
|
commitdiff
|
tree
2020-02-29
Andrew Reynolds
Replace conditional rewrite pass in quantifiers with...
commit
|
commitdiff
|
tree
2020-02-28
Andrew Reynolds
Use enum for quantifiers rewrite steps (#3840)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Refactor operator applications in the parser (#3831)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Update purifySygusGTerm to the new API (#3830)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Fix large models for strings (#3835)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Add support for is_digit and regular expression difference...
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Disable regression that times out on debug (#3833)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Move fix for vacuous sygus types out of the parser...
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
commit
|
commitdiff
|
tree
2020-02-27
Andrew Reynolds
Some initial work on using words (#3819)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Infrastructure for tautological literals in nonlinear...
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Use side effect utility for non-linear lemmas (#3780)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Fix regression (#3827)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
More fixes for printing sygus commands (#3812)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Refactor type ascriptions in the parser (#3825)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Minor improvement to ParseOp (#3808)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Use default consts when not using any const during...
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Fix node arity issue in reduction of int2bv (#3777)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Move equivalence class info to its own file in strings...
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Support for witnessing choice in models (#3781)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Minor cleaning of smt2 parser (#3823)
commit
|
commitdiff
|
tree
2020-02-26
Andrew Reynolds
Embed mkAssociative utilities within the API. (#3801)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Fixes for quantifiers documentation (#3811)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Utilities for words (#3797)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Convert parser input interface to api::Term (#3809)
commit
|
commitdiff
|
tree
2020-02-24
Andrew Reynolds
Add missing functions to new C++ API (#3769)
commit
|
commitdiff
|
tree
2020-02-23
Andrew Reynolds
Minor refactoring of equality notifications (#3798)
commit
|
commitdiff
|
tree
2020-02-22
Andrew Reynolds
Move check memberships to reg exp solver (#3793)
commit
|
commitdiff
|
tree
2020-02-22
Andrew Reynolds
Move cardinality inference scheme to base solver in...
commit
|
commitdiff
|
tree
2020-02-21
Andrew Reynolds
Simple changes towards unicode string standard (#3791)
commit
|
commitdiff
|
tree
2020-02-21
Andrew Reynolds
Split extended functions solver in strings (#3768)
commit
|
commitdiff
|
tree
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
commit
|
commitdiff
|
tree
2020-02-20
Andrew Reynolds
Minor removals (#3786)
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Fix symmetry breaking for multiple sygus types (#3775)
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Delay enumerative instantiation if theory engine does...
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Change Record to shared_ptr (#3778)
commit
|
commitdiff
|
tree
2020-02-19
Andrew Reynolds
Fix approximate bounds for transcendental functions...
commit
|
commitdiff
|
tree
2020-02-18
Andrew Reynolds
Add missing kinds for the new API (#3757)
commit
|
commitdiff
|
tree
2020-02-17
Andrew Reynolds
Option to limit the number of rounds of enumerative...
commit
|
commitdiff
|
tree
2020-02-17
Andrew Reynolds
Fix soundness bug in reduction of integer div/mod...
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Fix simple issue with cache (#3762)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Add temporary global API conversion utilities. (#3759)
commit
|
commitdiff
|
tree
2020-02-16
Andrew Reynolds
Disable regression (#3761)
commit
|
commitdiff
|
tree
2020-02-15
Andrew Reynolds
Move proxy variables to InferenceManager in strings...
commit
|
commitdiff
|
tree
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
commit
|
commitdiff
|
tree
2020-02-14
Andrew Reynolds
Update sygus v1 parser to use ParseOp utility (#3756)
commit
|
commitdiff
|
tree
2020-02-13
Andrew Reynolds
Const input for sygus print callback (#3755)
commit
|
commitdiff
|
tree
2020-02-12
Andrew Reynolds
Ensure ext rewrites for associative ops dont throw...
commit
|
commitdiff
|
tree
2020-02-12
Andrew Reynolds
Fix non-linear equality solving that involves mixed...
commit
|
commitdiff
|
tree
2020-02-11
Andrew Reynolds
Fix term simplification based on entailment in quantifiers...
commit
|
commitdiff
|
tree
2020-02-11
Andrew Reynolds
Use example evaluation cache instead of sygus PBE ...
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Fix rewrite rules sat regressions (#3734)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Split strings finite model finding strategy (#3727)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Split core solver from the theory of strings (#3713)
commit
|
commitdiff
|
tree
2020-02-08
Andrew Reynolds
Interface for example evaluation cache utilities (...
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Refactor check-model handling in SmtEngine (#3723)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Statistics for fast enumerator (#3699)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Example evaluation cache utility (#3698)
commit
|
commitdiff
|
tree
2020-02-07
Andrew Reynolds
Fix exact sqrt (#3721)
commit
|
commitdiff
|
tree
2020-02-06
Andrew Reynolds
Generalize containsQuantifiers to hasClosure (#3722)
commit
|
commitdiff
|
tree
2020-02-05
Andrew Reynolds
Fix QF_NIA smt comp script (#3715)
commit
|
commitdiff
|
tree
2020-02-04
Andrew Reynolds
Split base solver from the theory of strings (#3680)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Utility function for getting component types (#3703)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Minor fixes to regressions (#3702)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Split on model values when repaired model from non...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Fix invariant template inference for trivially infeasible...
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Fix corner case of empty domains in bounded fmf (#3690)
commit
|
commitdiff
|
tree
2020-02-03
Andrew Reynolds
Example inference utility (#3670)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Allow PBE symmetry breaking with sygus stream (#3686)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Refactor relevance vectors for asserted quantifiers...
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Update sygus grammar normalization to use node-level...
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Refactor sygus stats (#3684)
commit
|
commitdiff
|
tree
2020-01-31
Andrew Reynolds
Minor refactoring of constructor classes in fast enumerator...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Fix rep set increment for empty domains (#3682)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Make eq chain an aggressive rewrite in extended rewriter...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Eliminate spurious postprocessing step for single invocation...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Ensure literals in FMF decision strategies are in the...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Weaken assertion for models with approximations (#3667)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Move disequality list to solver state in strings (...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Example minimize evaluation utility. (#3671)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
External cache argument for evaluator (#3672)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Do not debug check model for models with approximations...
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Modularize more steps in the strings strategy (#3676)
commit
|
commitdiff
|
tree
2020-01-30
Andrew Reynolds
Minor updates to string utilities (#3675)
commit
|
commitdiff
|
tree
2020-01-29
Andrew Reynolds
Fix isLeq function in String utility (#3659)
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Do not insist on bound values being constant in arithmetic...
commit
|
commitdiff
|
tree
2020-01-28
Andrew Reynolds
Avoid PLUS with one child for bv2nat elimination (...
commit
|
commitdiff
|
tree
2020-01-23
Andrew Reynolds
Fix trivial solve method for single invocation (#3650)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix subtyping for instantiations where internal representati...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix substitution in nl solver (#3638)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix single invocation partition for non-function non...
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix check for subtypes in sygus PBE (#3640)
commit
|
commitdiff
|
tree
2020-01-22
Andrew Reynolds
Fix parameteric sorts involving Booleans in sygus default...
commit
|
commitdiff
|
tree
2020-01-17
Andrew Reynolds
Use axioms when checking goal entailment for abduction...
commit
|
commitdiff
|
tree
next