Sygus2 #1166
Sygus2 #1166
Conversation
| b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr | ||
| Partial.Err <$> | ||
| Partial.annotateME sym mop (NoSatisfyingWrite tp) b | ||
| -- b <- freshConstant sym (safeSymbol "noSatisfyingWrite") BaseBoolRepr |
There was a problem hiding this comment.
This should be controlled by some sort of config or saw option. The intent is to avoid very large sets of fresh constants due to the "trick".
| withFile "foo.smt2" WriteMode $ \handle -> | ||
| Z3.writeZ3HornSMT2File sym True handle uninterp_inv_fns implications | ||
| withFile "foo.sy" WriteMode $ \handle -> | ||
| CVC5.writeCVC5SyFile sym handle uninterp_inv_fns implications |
There was a problem hiding this comment.
Currently, always creates these files which record the attempted solver operation for examination in case of failure. Creating these should be configurable; used for debugging only.
| -- CVC5.runCVC5SyGuS sym logData uninterp_inv_fns implications >>= \case | ||
| -- Sat sub -> return sub | ||
| -- Unsat{} -> fail "Prover returned Infeasible" | ||
| -- Unknown -> fail "Prover returned Fail" |
There was a problem hiding this comment.
Needs to have some option to select which solver to use (other than commenting and recompiling as used here).
| -- checked. | ||
| -- | ||
| -- The basic use case here is for verifiying functions that loop | ||
| -- The basic use case here is for verifying functions that loop | ||
| -- through an array of data of symbolic length. This is done by | ||
| -- providing a \""fixpoint function\" which describes how the live | ||
| -- values in the loop at an arbitrary iteration are used to compute | ||
| -- the final values of those variables before execution leaves the | ||
| -- loop. The number and order of these variables depends on | ||
| -- internal details of the representation, so is relatively fragile. | ||
| simpleLoopFixpoint :: |
There was a problem hiding this comment.
This function is an extension/enhancement that does not impact other code and is only utilized when specifically utilizing this fixpoint feature, so while this is messy, it's relatively safe to include to prevent significant bitrot.
|
Superseded by #1178. |
No description provided.