projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix issues with unsat cores and reset-assertions (#4159)
[cvc5.git]
/
src
/
2020-03-27
Andres Noetzli
Fix issues with unsat cores and reset-assertions (...
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Move string utility file (#4164)
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Do not require that function sorts are first class...
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Move set defaults function to its own file (#4154)
tree
|
commitdiff
2020-03-26
Amalee
Added unit-cube-like test for branch and bound (#3922)
tree
|
commitdiff
2020-03-26
Andrew Reynolds
Add stats for string reductions, lemmas and conflicts...
tree
|
commitdiff
2020-03-26
Andrew Reynolds
Generalize more string-specific functions (#4152)
tree
|
commitdiff
2020-03-26
Andrew Reynolds
Care graphs based on polymorphic operators in strings...
tree
|
commitdiff
2020-03-25
Andres Noetzli
Support async-signal-safe printing of inferences (...
tree
|
commitdiff
2020-03-25
Ahmed Irfan
bv2int : linear mult opt (#4142)
tree
|
commitdiff
2020-03-25
Andrew Reynolds
Generalize more uses of string-specific functions...
tree
|
commitdiff
2020-03-24
yoni206
Int2BV fail on demand (#4079)
tree
|
commitdiff
2020-03-24
Andrew Reynolds
Restrict partial triggers to standard quantified formul...
tree
|
commitdiff
2020-03-24
Andrew Reynolds
Restrict cases of sygus grammar reduction based on...
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Infer when sygus operators are equivalent to builtin...
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Simplify auxiliary variable handling in CEGQI (#4141)
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Throw exception for non-well-founded unimplemented...
tree
|
commitdiff
2020-03-23
Andrew Reynolds
Change transcendental function app slave list to unorde...
tree
|
commitdiff
2020-03-23
Andres Noetzli
Collect statistics about normal form inferences (#4127)
tree
|
commitdiff
2020-03-22
Andrew Reynolds
Sort inference does not handle APPLY_UF when higher...
tree
|
commitdiff
2020-03-22
Abdalrhman Mohamed
Convert V1 Sygus files to V2. (#4136)
tree
|
commitdiff
2020-03-21
Andres Noetzli
Simplify heuristic in `processNEqc` (#4129)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Generalize mkConcat for types (#4123)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Fix variable shadowing issue in sygus-inference (#4121)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Fix sort comparison within assertion in cegis (#4113)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Guard cases of sort inference in quantifier free logics...
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Split string-specific operators from TheoryStringsRewri...
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Do not assign higher-order representative if function...
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Handle failures for sygus QE preprocess (#4072)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Parse error for SyGuS version 1.0 vs 2.0 (#4057)
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Make handling of illegal internal representatives in...
tree
|
commitdiff
2020-03-20
Andrew Reynolds
Refactor enumerator for strings (#4014)
tree
|
commitdiff
2020-03-19
yoni206
Bv2int fail on demand
tree
|
commitdiff
2020-03-19
Andres Noetzli
Only apply testConstStringInRegExp to const regexp...
tree
|
commitdiff
2020-03-19
Andrew Reynolds
SyGuS must use total bitvector division (#4119)
tree
|
commitdiff
2020-03-19
Andres Noetzli
Only allow bv2nat/int2bv with BV and integer logic...
tree
|
commitdiff
2020-03-19
Andrew Reynolds
Remove spurious assertion (#4117)
tree
|
commitdiff
2020-03-19
Andrew Reynolds
Explicitly handle isFinite for rounding modes (#4115)
tree
|
commitdiff
2020-03-19
Andrew Reynolds
Always enable cbqi literal dependency (#4116)
tree
|
commitdiff
2020-03-19
Andrew Reynolds
Fix issue with multiple infinities in CEGQI for LIRA...
tree
|
commitdiff
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
tree
|
commitdiff
2020-03-17
Aina Niemetz
SmtEngine: Convert members owned by SmtEngine to unique...
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Remove AlwaysAssert(false) for hole.
tree
|
commitdiff
2020-03-16
Alex Ozdemir
clang-format
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Fix simplicity check in prop
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Fix antecedent loop. Whoops
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Only save farkas+tightening proofs. Error on holes
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Expand the definition of a "simple" farkas proof.
tree
|
commitdiff
2020-03-16
Aina Niemetz
DecisionEngine: Use single unique pointer for ITE strat...
tree
|
commitdiff
2020-03-16
Andres Noetzli
Create master equality engine at context level 0 (...
tree
|
commitdiff
2020-03-16
Andrew Reynolds
Handle cases in --sygus-rr where evaluation is not...
tree
|
commitdiff
2020-03-13
Andrew Reynolds
Removing a few deprecated options (#4052)
tree
|
commitdiff
2020-03-13
Andrew Reynolds
Generalize type rules for strings to sequences (#3987)
tree
|
commitdiff
2020-03-13
Andrew Reynolds
Fix case of non-constant value for sygus sampling ...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Convert most instances of dataypes in parsers to the...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Do not allow quantifiers over real variables in real...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Remove local theory extension option (#4048)
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Do not make models for quantified function variables...
tree
|
commitdiff
2020-03-12
Aina Niemetz
New C++ API: Remove support for (reset). (#4037)
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Ensure legal candidate equalities when using relational...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Fix double notify in equality engine (#4036)
tree
|
commitdiff
2020-03-12
Aina Niemetz
Hide options for and related to the BV abstraction...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Simplifications to the Datatypes API (#4040)
tree
|
commitdiff
2020-03-12
makaimann
Add automatic Cython binding installation (#3933)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Do not enable some SMT-COMP specific options by default...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Guard against null relevancy condition in SyGuS (#4033)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Add missing datatype functions to new API (#3930)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Switch to Nodes for conjecture generator (#4026)
tree
|
commitdiff
2020-03-11
Andres Noetzli
reset-assertions: Update TheoryEngine's PropEngine...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Remove experimental symmetry breaker (#4005)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix non-parametrized operators in subgoal generation...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Remove partial instantiation for local theory extension...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix (#4017)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix duplicate variable issue in sygus-qe-preproc (...
tree
|
commitdiff
2020-03-11
Andres Noetzli
Introduce tables in the rewriter (#3742)
tree
|
commitdiff
2020-03-11
Andres Noetzli
Set assertion in `CnfStream::ensureLiteral()` (#3927)
tree
|
commitdiff
2020-03-11
Aina Niemetz
bv-gauss-elim: Fix handling of inconsistent case. ...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Fix real to int for parameterized kinds (#4016)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix sort inference for top-level Boolean variables...
tree
|
commitdiff
2020-03-10
Aina Niemetz
Fix issue with reset-assertions. (#3988)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Logic exception instead of assertion failure for instan...
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Remove assertion in resolution bound inferences (#3980)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Consolidate options that disable produceModels (#3973)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix assertion failure in sort inference for Boolean...
tree
|
commitdiff
2020-03-10
Aina Niemetz
Fix -Wshadow warnings in sygus_grammar_cons.cpp. (...
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Do not set values for non-linear mult terms in collectM...
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Fix real as int for incremental (#3979)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Do not traverse quantifiers in nl ext purify (#3982)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Only register sygus terms to unfold if option is set...
tree
|
commitdiff
2020-03-10
Alex Ozdemir
Document bv-to-bool recursion (#3848)
tree
|
commitdiff
2020-03-10
makaimann
Enhancement: make the bool-to-bv pass more robust and...
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Rename sygus option name (#3977)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Remove instantiation propagator infrastructure (#3975)
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Ensure standard miniscoping is applied before aggressiv...
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Eliminate spurious assertion (#3976)
tree
|
commitdiff
2020-03-09
Aina Niemetz
DecisionEngine: Use unique_ptr for enabled strategies...
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Fix type issue in arith rewrite equality (#3972)
tree
|
commitdiff
2020-03-09
Andres Noetzli
Make registration of unit clauses more robust (#3965)
tree
|
commitdiff
2020-03-09
Andrew Reynolds
Clean up more uses of ExprManager in parsers (#3932)
tree
|
commitdiff
next