Skip to content

Commit

Permalink
use real(.) and imag(.) in place of .R and .I when parsing predicates
Browse files Browse the repository at this point in the history
  • Loading branch information
alan23273850 committed Aug 27, 2024
1 parent 550dedd commit 8aab340
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 1 deletion.
2 changes: 1 addition & 1 deletion benchmarks/LSTA/OEGrover/02/post.hsl
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Predicates
p := (and (> (* $R $R) (* bR bR)) (= $I 0))
p := (and (> (* real($) real($)) (* real(b) real(b))) (= imag($) 0))
t := true
Extended Dirac
p|011> + t|*>
5 changes: 5 additions & 0 deletions src/inclusion.cc
Original file line number Diff line number Diff line change
Expand Up @@ -379,6 +379,11 @@ bool AUTOQ::Automata<AUTOQ::Symbol::Index>::operator<=(const Automata<AUTOQ::Sym

bool AUTOQ::check_validity(Constraint C, const PredicateAutomata::Symbol &ps, const SymbolicAutomata::Symbol &te) {
std::string str(ps);
/* Replace all real(.) in C.content with .R and
replace all imag(.) in C.content with .I */
str = std::regex_replace(str, std::regex("real\\((.*?)\\)"), "$1R");
str = std::regex_replace(str, std::regex("imag\\((.*?)\\)"), "$1I");
/******************************************************************/
auto regToExpr = C.to_exprs(te);
for (const auto &kv : regToExpr) // example: z3 <(echo '(declare-fun x () Int)(declare-fun z () Int)(assert (= z (+ x 3)))(check-sat)')
str = std::regex_replace(str, std::regex(kv.first), kv.second);
Expand Down

0 comments on commit 8aab340

Please sign in to comment.