Skip to content

Commit

Permalink
Minor changes
Browse files Browse the repository at this point in the history
  • Loading branch information
racoucho1u committed Jul 22, 2022
1 parent 170d075 commit 1845a45
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
4 changes: 2 additions & 2 deletions lib/theory/src/Theory/Constraint/Solver/ProofMethod.hs
Original file line number Diff line number Diff line change
Expand Up @@ -623,7 +623,7 @@ itRanking tactic ags ctxt _sys = result
prioToFunctions = map functionsPrio (_prios tactic)
indexPrio = map (findIndex (==True)) $ map (applyIsPrio prioToFunctions ctxt _sys) ags -- find the first prio that match every goal
indexedPrio = sortOn fst $ zip indexPrio ags -- ordening of goals given the fisrt prio they meet
groupedPrio = trace ("Hellooooooo\n" ++ show indexedPrio) groupBy (\(indice1,_) (indice2,_) -> indice1 == indice2) indexedPrio -- grouping goals by prio
groupedPrio = groupBy (\(indice1,_) (indice2,_) -> indice1 == indice2) indexedPrio -- grouping goals by prio
preorderedPrio = if (Nothing `elem` indexPrio) then map (snd . unzip) (tail groupedPrio) else map (snd . unzip) groupedPrio -- recovering ranked goals only (no prio = Nothing = fst)

prioRankingFunctions = map rankingPrio (_prios tactic)
Expand Down Expand Up @@ -694,7 +694,7 @@ internalTacticRanking tactic ctxt _sys ags0 =
let logMsg = ">>>>>>>>>>>>>>>>>>>>>>>> START INPUT\n"
++ inp
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> START OUTPUT\n"
++ show pretttOut
++ prettyOut
++ "\n>>>>>>>>>>>>>>>>>>>>>>>> END Oracle call\n"
guard $ trace logMsg True
return (res)
Expand Down
2 changes: 1 addition & 1 deletion lib/theory/src/Theory/Text/Parser/Tactics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ tacticFunctions = M.fromList
sysPattern = "~n":(map show $ concat (map (checkFormula oracleType) (S.toList $ L.get sFormulas sys)))

checkFormula :: String -> LNGuarded -> [LVar]
checkFormula oracleType f = if rev && expG then trace (show $ concat $ getFormulaTermsCore f ) concat $ getFormulaTermsCore f else []
checkFormula oracleType f = if rev && expG then concat $ getFormulaTermsCore f else []

where
rev = or $ map matchReveal (map factTagName $ guardFactTags f)
Expand Down

0 comments on commit 1845a45

Please sign in to comment.