diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-03 09:18:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-03 09:18:59 -0600 |
commit | 0cd812af4a6db43a7d6c2c95fff7e58f86e90a78 (patch) | |
tree | ab35d8c8dd7ee7c7c8ba085d42ef834fe17e2dbd /src/theory/builtin/kinds | |
parent | 1d44edf91762b837adf3db5ed40af9383e883b28 (diff) |
Standardize the interface for SMT engine subsolvers (#3836)
This standardizes the interface for using SMT engines as subsolvers in various approaches. More refactoring is possible, but this is an initial cut at cleaning things up.
This will make it easy to accommodate new feature request for SyGuS (timeouts for calls to verification steps).
Notice this also required adding a missing function (mkGroundTerm/isWellFounded for functions) which was caught after standardizing due to an optimization (don't create SmtEngines to check satisfiability of constant Booleans).
Diffstat (limited to 'src/theory/builtin/kinds')
-rw-r--r-- | src/theory/builtin/kinds | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index c90419def..4d5e95119 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -309,7 +309,10 @@ operator FUNCTION_TYPE 2: "a function type" cardinality FUNCTION_TYPE \ "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -well-founded FUNCTION_TYPE false +well-founded FUNCTION_TYPE \ + "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" enumerator FUNCTION_TYPE \ ::CVC4::theory::builtin::FunctionEnumerator \ "theory/builtin/type_enumerator.h" |